diff options
Diffstat (limited to 'Test/test2/AssumptionVariables0.bpl')
-rw-r--r-- | Test/test2/AssumptionVariables0.bpl | 113 |
1 files changed, 73 insertions, 40 deletions
diff --git a/Test/test2/AssumptionVariables0.bpl b/Test/test2/AssumptionVariables0.bpl index cc73707c..84bf14ad 100644 --- a/Test/test2/AssumptionVariables0.bpl +++ b/Test/test2/AssumptionVariables0.bpl @@ -1,40 +1,73 @@ -// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure Test0()
-{
- var {:assumption} a0: bool;
-
- assert a0;
-}
-
-
-procedure Test1(n: int)
-{
- var {:assumption} a0: bool;
-
- a0 := a0 && (0 <= n);
-
- assert a0; // error
-}
-
-
-procedure Test2()
-{
- var {:assumption} a0: bool;
-
- havoc a0;
-
- assert a0; // error
-}
-
-
-var {:assumption} a0: bool;
-
-
-procedure Test3()
- modifies a0;
-{
- a0 := a0 && true;
-
- assert a0; // error
-}
+// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure Test0() +{ + var {:assumption} a0: bool; + + assert a0; +} + + +procedure Test1(n: int) +{ + var {:assumption} a0: bool; + + a0 := a0 && (0 <= n); + + assert a0; // error +} + + +procedure Test2() +{ + var {:assumption} a0: bool; + + havoc a0; + + assert a0; // error +} + + +var {:assumption} ga0: bool; + + +procedure Test3() + modifies ga0; +{ + ga0 := ga0 && true; + + 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; +} |