From 43b80b13bd24bb789849aac3385df6ac4a8233be Mon Sep 17 00:00:00 2001
From: boehmes <unknown>
Date: Thu, 27 Sep 2012 17:13:45 +0200
Subject: 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)

---
 Test/test1/Answer      | 19 +++++++++++++++++++
 Test/test1/IntReal.bpl | 48 ++++++++++++++++++++++++++++++++++++++++++++++++
 Test/test1/runtest.bat |  1 +
 3 files changed, 68 insertions(+)
 create mode 100644 Test/test1/IntReal.bpl

(limited to 'Test/test1')

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
-- 
cgit v1.2.3