diff options
| author |  Dietrich <dgeisler50@gmail.com> | 2015-04-20 05:20:06 -0600 |
|---|---|---|
| committer | Dietrich <dgeisler50@gmail.com> | 2015-04-20 05:20:06 -0600 |
| commit | 4f35766542c5735374b85f66006afea875f07b79 (patch) | |
| tree | 76842d97212c417a28baf425e9b30fb2a6ecf3f7 | |
| parent | bdb6a7db94de0310fb6535facb33782fe231c013 (diff) | |
added a collection of console writes for debugging. These should be removed in a future commit
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 2 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 2 | ||||
| -rw-r--r-- | Source/Core/Scanner.cs | 3 | ||||
| -rw-r--r-- | 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 |