From 25168d775055ca464bb5cc57120f7caff8924779 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Tue, 27 May 2014 16:16:52 +0200
Subject: Implemented an additional type check for assumption variables.

---
 Test/test1/Answer                          | 2 ++
 Test/test1/AssumptionVariables1.bpl        | 6 ++++++
 Test/test1/AssumptionVariables1.bpl.expect | 2 ++
 Test/test1/runtest.bat                     | 1 +
 4 files changed, 11 insertions(+)
 create mode 100644 Test/test1/AssumptionVariables1.bpl
 create mode 100644 Test/test1/AssumptionVariables1.bpl.expect

(limited to 'Test/test1')

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