summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-05-27 16:16:52 +0200
committerGravatar wuestholz <unknown>2014-05-27 16:16:52 +0200
commit25168d775055ca464bb5cc57120f7caff8924779 (patch)
tree303fe6ec5d4ec2a63d54b133ab089912b6413618 /Test
parente0a7d0330df42841c0c18a7439b1d60abf7703c9 (diff)
Implemented an additional type check for assumption variables.
Diffstat (limited to 'Test')
-rw-r--r--Test/test1/Answer2
-rw-r--r--Test/test1/AssumptionVariables1.bpl6
-rw-r--r--Test/test1/AssumptionVariables1.bpl.expect2
-rw-r--r--Test/test1/runtest.bat1
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