From b17515ca23fc7f5ae1fb8e6642366f761d0eeacf Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 21 Apr 2014 13:21:52 +0200
Subject: Add support for assumption variables.

---
 Test/test1/Answer                   |  6 ++++
 Test/test1/AssumptionVariables0.bpl | 55 +++++++++++++++++++++++++++++++++++++
 Test/test1/runtest.bat              |  1 +
 3 files changed, 62 insertions(+)
 create mode 100644 Test/test1/AssumptionVariables0.bpl

(limited to 'Test/test1')

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