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 | |
| 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')
| -rw-r--r-- | Test/test2/AssumptionVariables0.bpl | 41 | ||||
| -rw-r--r-- | Test/test2/AssumptionVariables0.bpl.expect | 22 |
2 files changed, 48 insertions, 15 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;
}
diff --git a/Test/test2/AssumptionVariables0.bpl.expect b/Test/test2/AssumptionVariables0.bpl.expect index 54ddb2a9..44292082 100644 --- a/Test/test2/AssumptionVariables0.bpl.expect +++ b/Test/test2/AssumptionVariables0.bpl.expect @@ -1,11 +1,11 @@ -AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold. -Execution trace: - AssumptionVariables0.bpl(15,8): anon0 -AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold. -Execution trace: - AssumptionVariables0.bpl(25,5): anon0 -AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold. -Execution trace: - AssumptionVariables0.bpl(37,8): anon0 - -Boogie program verifier finished with 1 verified, 3 errors +AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssumptionVariables0.bpl(15,8): anon0
+AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssumptionVariables0.bpl(25,5): anon0
+AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssumptionVariables0.bpl(37,9): anon0
+
+Boogie program verifier finished with 3 verified, 3 errors
|