diff options
| author |  Rustan Leino <unknown> | 2014-02-10 18:54:56 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-10 18:54:56 -0800 |
| commit | 7632fe2542f138a83ee3a9b39d5bcad09cd5fcf7 (patch) | |
| tree | 64f05c4a234fb3bfda727bd9f151b2dcd9a988d1 /Test | |
| parent | 8567d68f7f04f87b2d4270e18713bdcdf4d26031 (diff) | |
Fixed bug in printing real literals
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/test21/Answer | 30 | ||||
| -rw-r--r-- | Test/test21/Real.bpl | 45 |
2 files changed, 71 insertions, 4 deletions
diff --git a/Test/test21/Answer b/Test/test21/Answer index 3ae659ec..73feaf41 100644 --- a/Test/test21/Answer +++ b/Test/test21/Answer @@ -279,8 +279,16 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
--------------------- File Real.bpl ----------------------------
+Real.bpl(26,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Real.bpl(23,5): anon0
+ Real.bpl(26,5): anon3_Then
+Real.bpl(41,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Real.bpl(34,3): anon0
+ Real.bpl(41,5): anon3_Else
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 2 verified, 2 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
@@ -556,8 +564,16 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
--------------------- File Real.bpl ----------------------------
+Real.bpl(26,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Real.bpl(23,5): anon0
+ Real.bpl(26,5): anon3_Then
+Real.bpl(41,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Real.bpl(34,3): anon0
+ Real.bpl(41,5): anon3_Else
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 2 verified, 2 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
@@ -836,8 +852,16 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
--------------------- File Real.bpl ----------------------------
+Real.bpl(26,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Real.bpl(23,5): anon0
+ Real.bpl(26,5): anon3_Then
+Real.bpl(41,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Real.bpl(34,3): anon0
+ Real.bpl(41,5): anon3_Else
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 2 verified, 2 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl index 3dcf3ea3..c9a2f14d 100644 --- a/Test/test21/Real.bpl +++ b/Test/test21/Real.bpl @@ -14,4 +14,47 @@ procedure P(a: real, b: real) returns () { assert a != 0.0 ==> a / a == 1.0;
assert int(a) >= 0 ==> real(3) * a > a;
-}
\ No newline at end of file +}
+
+procedure ManyDigitReals()
+{
+ var x: real;
+ var y: real;
+ x := 15e-1;
+ y := real(3);
+ if (*) {
+ assert x == y / 2000000000000000000000000001e-27; // error
+ } else {
+ assert x == y / 2000000000000000000000000000e-27;
+ }
+}
+
+procedure Rounding()
+{
+ assert real(3) == 3.0;
+ assert int(2.2) == int(2.8);
+ assert int(2.2) == 2;
+ assert int(-2.2) == int(-2.8);
+ if (*) {
+ assert int(-2.2) == -3;
+ } else {
+ assert int(-2.2) == -2; // error: int truncates downward
+ }
+}
+
+procedure VariousCornerCaseBigDecPrintingTests()
+{
+ assert 200e-2 == 2.0;
+ assert 000e-2 == 0.0;
+ assert 000e-1 == 0.0;
+ assert 000e-4 == 0.0;
+ assert 000e0 == 0.0;
+ assert 0e-300 == 0.0;
+ assert 12300e-4 == 1.230;
+ assert 12300e-5 == 0.123;
+ assert 12300e-8 == 000.000123;
+ assert 1.9850404e5 == 198504.04;
+ assert 19850404e-4 == 1985.0404;
+ assert 19850404e-12 == 0.00001985040400000;
+ assert 19850404e0000000000000000 == 1985.0404e4;
+}
|