Implemented an additional type check for assumption variables.

4 files changed, 11 insertions, 0 deletions

diff --git a/Test/test1/Answer b/Test/test1/Answer
index 403b4289..aff9894c 100644
--- a/Test/test1/Answer
+++ b/Test/test1/Answer
@@ -166,3 +166,5 @@ AssumptionVariables0.bpl(30,7): Error: RHS of assignment to assumption variable
 AssumptionVariables0.bpl(39,7): Error: assumption variable may not be assigned to more than once

 AssumptionVariables0.bpl(56,7): Error: assumption variable may not be assigned to more than once

 5 name resolution errors detected in AssumptionVariables0.bpl

+AssumptionVariables1.bpl(5,22): Error: assumption variable must be of type 'bool'

+1 type checking errors detected in AssumptionVariables1.bpl

diff --git a/Test/test1/AssumptionVariables1.bpl b/Test/test1/AssumptionVariables1.bpl
new file mode 100644
index 00000000..dea71396
--- /dev/null
+++ b/Test/test1/AssumptionVariables1.bpl
@@ -0,0 +1,6 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

+procedure Test0()

+{

+    var {:assumption} a0: int;  // error

+}

diff --git a/Test/test1/AssumptionVariables1.bpl.expect b/Test/test1/AssumptionVariables1.bpl.expect
new file mode 100644
index 00000000..9e894bf9
--- /dev/null
+++ b/Test/test1/AssumptionVariables1.bpl.expect
@@ -0,0 +1,2 @@
+AssumptionVariables1.bpl(5,22): Error: assumption variable must be of type 'bool'

+1 type checking errors detected in AssumptionVariables1.bpl

diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat
index c8044836..9225d5f7 100644
--- a/Test/test1/runtest.bat
+++ b/Test/test1/runtest.bat
@@ -20,3 +20,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe
 %BGEXE% %* /noVerify Lambda.bpl

 %BGEXE% %* /noVerify IntReal.bpl

 %BGEXE% %* /noVerify AssumptionVariables0.bpl

+%BGEXE% %* /noVerify AssumptionVariables1.bpl