diff options
| author |  wuestholz <unknown> | 2014-04-21 13:21:52 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-04-21 13:21:52 +0200 |
| commit | b17515ca23fc7f5ae1fb8e6642366f761d0eeacf (patch) | |
| tree | 1f1b42a681dab35e9d6aa02bc1a79d01c113c82f /Test/test1 | |
| parent | c29f461136e76fd406677e1e12245ee69368190f (diff) | |
Add support for assumption variables.
Diffstat (limited to 'Test/test1')
| -rw-r--r-- | Test/test1/Answer | 6 | ||||
| -rw-r--r-- | Test/test1/AssumptionVariables0.bpl | 55 | ||||
| -rw-r--r-- | Test/test1/runtest.bat | 1 |
3 files changed, 62 insertions, 0 deletions
diff --git a/Test/test1/Answer b/Test/test1/Answer index e1a36ad9..b79a01f8 100644 --- a/Test/test1/Answer +++ b/Test/test1/Answer @@ -160,3 +160,9 @@ 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
+AssumptionVariables0.bpl(3,22): Error: assumption variable may not be declared with a where clause
+AssumptionVariables0.bpl(19,7): Error: RHS of assignment to assumption variable a0 must match expression "a0 && <boolean expression>"
+AssumptionVariables0.bpl(28,7): Error: RHS of assignment to assumption variable a0 must match expression "a0 && <boolean expression>"
+AssumptionVariables0.bpl(37,7): Error: assumption variable may not be assigned to more than once
+AssumptionVariables0.bpl(54,7): Error: assumption variable may not be assigned to more than once
+5 name resolution errors detected in AssumptionVariables0.bpl
diff --git a/Test/test1/AssumptionVariables0.bpl b/Test/test1/AssumptionVariables0.bpl new file mode 100644 index 00000000..4185ffd3 --- /dev/null +++ b/Test/test1/AssumptionVariables0.bpl @@ -0,0 +1,55 @@ +procedure Test0()
+{
+ var {:assumption} a0: bool where a0; // error
+}
+
+
+procedure Test1()
+{
+ var {:assumption} a0: bool;
+
+ a0 := a0 && true;
+}
+
+
+procedure Test2()
+{
+ var {:assumption} a0: bool;
+
+ a0 := true; // error
+}
+
+
+procedure Test3()
+{
+ var {:assumption} a0: bool;
+ var {:assumption} a1: bool;
+
+ a0 := a1 && true; // error
+}
+
+
+procedure Test4()
+{
+ var {:assumption} a0: bool;
+
+ a0 := a0 && true;
+ a0 := a0 && true; // error
+}
+
+
+procedure Test5()
+ modifies a0;
+{
+ a0 := a0 && true;
+}
+
+
+var {:assumption} a0: bool;
+
+
+procedure Test6()
+ modifies a0;
+{
+ a0 := a0 && true; // error
+}
diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat index ccd04355..c8044836 100644 --- a/Test/test1/runtest.bat +++ b/Test/test1/runtest.bat @@ -19,3 +19,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe %BGEXE% %* /noVerify IfThenElse0.bpl
%BGEXE% %* /noVerify Lambda.bpl
%BGEXE% %* /noVerify IntReal.bpl
+%BGEXE% %* /noVerify AssumptionVariables0.bpl
|