diff options
Diffstat (limited to 'Test/test1/AssumptionVariables0.bpl')
-rw-r--r-- | Test/test1/AssumptionVariables0.bpl | 55 |
1 files changed, 55 insertions, 0 deletions
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
+}
|