From 4f35766542c5735374b85f66006afea875f07b79 Mon Sep 17 00:00:00 2001
From: Dietrich <dgeisler50@gmail.com>
Date: Mon, 20 Apr 2015 05:20:06 -0600
Subject: added a collection of console writes for debugging.  These should be
 removed in a future commit

---
 Source/Core/AbsyExpr.cs |  2 ++
 Source/Core/Parser.cs   |  2 ++
 Source/Core/Scanner.cs  |  3 +++
 float_test.bpl          | 12 +++---------
 4 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 62145eed..7aa457fe 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -630,6 +630,8 @@ namespace Microsoft.Boogie {
           return Type.Int;
         } else if (Val is BigDec) {
           return Type.Real;
+        } else if (Val is FP32) {
+          return Type.Float;
         } else if (Val is BvConst) {
           return Type.GetBvType(((BvConst)Val).Bits);
         } else {
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 5545d8c4..bbe7af4b 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -170,6 +170,7 @@ private class BvBounds : Expr {
 		for (;;) {
 			t = la;
 			la = scanner.Scan();
+   Console.WriteLine("Just got the value " + la.kind + " with value " + la.val);
 			if (la.kind <= maxT) { ++errDist; break; }
 
 			la = t;
@@ -597,6 +598,7 @@ private class BvBounds : Expr {
 
 	void Type(out Bpl.Type/*!*/ ty) {
 		Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType; 
+  Console.WriteLine(la.kind + " from parser.Type");
 		if (StartOf(5)) {
 			TypeAtom(out ty);
 		} else if (la.kind == 1) {
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index a3c139c8..2df118d6 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -502,6 +502,7 @@ public class Scanner {
 
 
 	void CheckLiteral() {
+   Console.Write(t.val + " is a literal");
 		switch (t.val) {
 			case "var": t.kind = 7; break;
 			case "where": t.kind = 13; break;
@@ -548,6 +549,7 @@ public class Scanner {
 			case "lambda": t.kind = 92; break;
 			default: break;
 		}
+  Console.WriteLine(" and is kind " + t.kind);
 	}
 
 	Token/*!*/ NextToken() {
@@ -777,6 +779,7 @@ public class Scanner {
 
 		}
 		t.val = new String(tval, 0, tlen);
+  Console.WriteLine("Scanning a token with value " + t._val);
 		return t;
 	}
 
diff --git a/float_test.bpl b/float_test.bpl
index 22e436a1..ebd0ab47 100644
--- a/float_test.bpl
+++ b/float_test.bpl
@@ -1,11 +1,5 @@
-procedure F(n: int) returns (r: int)
-  ensures 100 < n ==> r == n - 10;  // This postcondition is easy to check by hand
-  ensures n <= 100 ==> r == 91;     // Do you believe this one is true?
+procedure F(n: float) returns(r: float)
+	ensures r == n;
 {
-  if (100 < n) {
-    r := n - 10;
-  } else {
-    call r := F(n + 11);
-    call r := F(r);
-  }
+	r := n;
 }
\ No newline at end of file
-- 
cgit v1.2.3