diff options
| author |  boehmes <unknown> | 2012-09-27 17:13:45 +0200 |
|---|---|---|
| committer | boehmes <unknown> | 2012-09-27 17:13:45 +0200 |
| commit | 43b80b13bd24bb789849aac3385df6ac4a8233be (patch) | |
| tree | 499b3dffd74fd84fdf8aedffacbca424d25680b2 /Test/test21 | |
| parent | dfb77ee06c82cf8b9c465f3a2acbc5ceb035c6e5 (diff) | |
Boogie: added type 'real' with overloaded arithmetic operations plus real division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real';
Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted;
Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs);
Extended the BigDec class with additional functionality;
Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
Diffstat (limited to 'Test/test21')
| -rw-r--r-- | Test/test21/Answer | 9 | ||||
| -rw-r--r-- | Test/test21/Real.bpl | 17 | ||||
| -rw-r--r-- | Test/test21/runtest.bat | 4 |
3 files changed, 29 insertions, 1 deletions
diff --git a/Test/test21/Answer b/Test/test21/Answer index 914e56a1..28aa4e8b 100644 --- a/Test/test21/Answer +++ b/Test/test21/Answer @@ -278,6 +278,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
+--------------------- File Real.bpl ----------------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
@@ -549,6 +552,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
+--------------------- File Real.bpl ----------------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
@@ -826,6 +832,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
+--------------------- File Real.bpl ----------------------------
+
+Boogie program verifier finished with 1 verified, 0 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 new file mode 100644 index 00000000..3dcf3ea3 --- /dev/null +++ b/Test/test21/Real.bpl @@ -0,0 +1,17 @@ +axiom (forall r: real :: r == 0.0 || r / r == 1.0);
+
+procedure P(a: real, b: real) returns () {
+ assume a >= b && a != 0.0 && a >= 1.3579;
+
+ assert 2e0 * (a + 3.0) - 0.5 >= b;
+ assert 2e0 * (a + 3.0) - 0.5 > b;
+ assert b <= 2e0 * (a + 3.0) - 0.5;
+ assert b < 2e0 * (a + 3.0) - 0.5;
+
+ assert 1/2 <= 0.65;
+ assert a > 100e-2 ==> 1 / a <= a;
+ assert a / 2 != a || a == 0.00;
+ assert a != 0.0 ==> a / a == 1.0;
+
+ assert int(a) >= 0 ==> real(3) * a > a;
+}
\ No newline at end of file diff --git a/Test/test21/runtest.bat b/Test/test21/runtest.bat index d994a4da..bfdcc570 100644 --- a/Test/test21/runtest.bat +++ b/Test/test21/runtest.bat @@ -4,6 +4,7 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
rem set BGEXE=mono ..\..\Binaries\Boogie.exe
+
for %%m in (
n p a
) do (
@@ -16,7 +17,8 @@ for %%f in (DisjointDomains.bpl DisjointDomains2.bpl FunAxioms.bpl Keywords.bpl Casts.bpl BooleanQuantification.bpl EmptyList.bpl Boxing.bpl
MapOutputTypeParams.bpl ParallelAssignment.bpl BooleanQuantification2.bpl
Flattening.bpl Orderings.bpl Orderings2.bpl Orderings3.bpl Orderings4.bpl
- EmptySetBug.bpl Coercions2.bpl MapAxiomsConsistency.bpl LargeLiterals0.bpl) do (
+ EmptySetBug.bpl Coercions2.bpl MapAxiomsConsistency.bpl LargeLiterals0.bpl
+ Real.bpl) do (
echo --------------------- File %%f ----------------------------
%BGEXE% %* /typeEncoding:%%m /logPrefix:0%%m %%f
)
|