diff options
| author |  Valentin Wüstholz <wuestholz@gmail.com> | 2015-05-06 17:52:52 +0200 |
|---|---|---|
| committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-05-06 17:52:52 +0200 |
| commit | c09814e1ae44a0bee53abb6e8e65b79c1da03d9e (patch) | |
| tree | 4f13bb3b1797e544a204823b5913272a5f818714 /Test/test2/AssumptionVariables0.bpl | |
| parent | 0901edfa9185f2e2bbd331130b391dd1dda06f16 (diff) | |
Make it preserve the fact that the value of an assumption variable never becomes logically weaker after a havoc.
Diffstat (limited to 'Test/test2/AssumptionVariables0.bpl')
| -rw-r--r-- | Test/test2/AssumptionVariables0.bpl | 41 |
1 files changed, 37 insertions, 4 deletions
diff --git a/Test/test2/AssumptionVariables0.bpl b/Test/test2/AssumptionVariables0.bpl index cc73707c..766c9d1e 100644 --- a/Test/test2/AssumptionVariables0.bpl +++ b/Test/test2/AssumptionVariables0.bpl @@ -28,13 +28,46 @@ procedure Test2() }
-var {:assumption} a0: bool;
+var {:assumption} ga0: bool;
procedure Test3()
- modifies a0;
+ modifies ga0;
{
- a0 := a0 && true;
+ ga0 := ga0 && true;
- assert a0; // error
+ assert ga0; // error
+}
+
+
+procedure Test4()
+{
+ var {:assumption} a0: bool;
+ var tmp: bool;
+
+ tmp := a0;
+
+ havoc a0;
+
+ assert a0 ==> tmp;
+}
+
+
+procedure Test5(A: bool)
+{
+ var {:assumption} a0: bool;
+ var tmp0, tmp1: bool;
+
+ a0 := a0 && A;
+ tmp0 := a0;
+
+ havoc a0;
+
+ assert a0 ==> tmp0;
+
+ tmp1 := a0;
+
+ havoc a0;
+
+ assert a0 ==> tmp1;
}
|