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/test1 | |
| 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/test1')
| -rw-r--r-- | Test/test1/Answer | 19 | ||||
| -rw-r--r-- | Test/test1/IntReal.bpl | 48 | ||||
| -rw-r--r-- | Test/test1/runtest.bat | 1 |
3 files changed, 68 insertions, 0 deletions
diff --git a/Test/test1/Answer b/Test/test1/Answer index a8b73b53..94bf2d9a 100644 --- a/Test/test1/Answer +++ b/Test/test1/Answer @@ -145,3 +145,22 @@ Lambda.bpl(12,8): Error: the type variable T does not occur in types of the lamb Lambda.bpl(12,2): Error: mismatched types in assignment command (cannot assign <T>[int]int to [int]int)
Lambda.bpl(18,27): Error: invalid argument types (bool and int) to binary operator +
5 type checking errors detected in Lambda.bpl
+IntReal.bpl(5,8): Error: invalid argument types (int and real) to binary operator >=
+IntReal.bpl(6,8): Error: invalid argument types (int and real) to binary operator <=
+IntReal.bpl(7,8): Error: invalid argument types (int and real) to binary operator <
+IntReal.bpl(8,8): Error: invalid argument types (int and real) to binary operator >
+IntReal.bpl(10,9): Error: invalid argument types (int and real) to binary operator ==
+IntReal.bpl(11,8): Error: invalid argument types (int and real) to binary operator +
+IntReal.bpl(12,8): Error: invalid argument types (int and real) to binary operator -
+IntReal.bpl(13,8): Error: invalid argument types (int and real) to binary operator *
+IntReal.bpl(14,8): Error: invalid argument types (int and real) to binary operator div
+IntReal.bpl(15,8): Error: invalid argument types (int and real) to binary operator mod
+IntReal.bpl(17,12): Error: invalid argument types (real and int) to binary operator ==
+IntReal.bpl(23,8): Error: invalid argument types (int and real) to binary operator **
+IntReal.bpl(27,14): Error: invalid argument types (real and int) to binary operator ==
+IntReal.bpl(29,13): Error: invalid argument types (int and real) to binary operator ==
+IntReal.bpl(32,6): Error: argument type int does not match expected type real
+IntReal.bpl(33,6): Error: argument type real does not match expected type int
+IntReal.bpl(45,8): Error: invalid argument types (real and int) to binary operator div
+IntReal.bpl(46,8): Error: invalid argument types (real and int) to binary operator mod
+18 type checking errors detected in IntReal.bpl
\ No newline at end of file diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl new file mode 100644 index 00000000..fac41d57 --- /dev/null +++ b/Test/test1/IntReal.bpl @@ -0,0 +1,48 @@ +const i: int;
+const r: real;
+
+axiom i == 0;
+axiom i >= 0.0; // type errror
+axiom i <= 0.0e0; // type errror
+axiom i < 0.0e-0; // type errror
+axiom i > 0.0e20; // type errror
+
+axiom -i == r; // type errror
+axiom i + r == 0.0; // type errror
+axiom i - r == 0.0; // type errror
+axiom i * r == 0.0; // type errror
+axiom i div r == 0; // type errror
+axiom i mod r == 0; // type errror
+
+axiom i / i == 0; // type errror
+axiom i / i == 0.0;
+axiom i / r == 0.0;
+axiom r / i == 0.0;
+axiom r / r == 0.0;
+
+axiom i ** r == 0.0; // type errror
+axiom r ** r == 0.0;
+
+axiom real(i) == 0.0;
+axiom real(i) == i; // type errror
+axiom int(r) == 0;
+axiom int(r) == r; // type errror
+axiom int(real(i)) == i;
+axiom real(int(r)) == r;
+axiom int(int(r)) == i; // type errror
+axiom real(real(i)) == r; // type errror
+
+axiom i == 0;
+axiom real(i) >= 0.0;
+axiom real(i) <= 0.0e0;
+axiom r < 0.0e-0;
+axiom r > 0.0e20;
+
+axiom -r == real(i);
+axiom real(i) + r == 0.0;
+axiom r - real(0) == 0.0;
+axiom r * r == 0.0;
+axiom r div 0 == 0; // type errror
+axiom r mod 0 == 0; // type errror
+
+axiom r ** r == 0.0;
diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat index 979c36e4..149e6dc9 100644 --- a/Test/test1/runtest.bat +++ b/Test/test1/runtest.bat @@ -19,3 +19,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe %BGEXE% %* /noVerify FunBody.bpl
%BGEXE% %* /noVerify IfThenElse0.bpl
%BGEXE% %* /noVerify Lambda.bpl
+%BGEXE% %* /noVerify IntReal.bpl
|