diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
| commit | 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch) | |
| tree | 27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Test/AbsHoudini | |
| parent | e11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff) | |
Normalise line endings using a .gitattributes file. Unfortunately
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
Diffstat (limited to 'Test/AbsHoudini')
34 files changed, 1485 insertions, 1485 deletions
diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer index f0136d80..2ab37f22 100644 --- a/Test/AbsHoudini/Answer +++ b/Test/AbsHoudini/Answer @@ -1,489 +1,489 @@ -
--------------------- houd1.bpl --------------------
-function {:existential true} {:inline} b1(x: bool) : bool
-{
- true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd2.bpl --------------------
-function {:existential true} {:inline} Assert(x: bool) : bool
-{
- true
-}
-function {:existential true} {:inline} b1(x: bool) : bool
-{
- true
-}
-function {:existential true} {:inline} b2(x: bool) : bool
-{
- false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd3.bpl --------------------
-function {:existential true} {:inline} Assert(x: bool) : bool
-{
- x
-}
-function {:existential true} {:inline} b1(x: bool) : bool
-{
- true
-}
-function {:existential true} {:inline} b2(x: bool) : bool
-{
- true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd4.bpl --------------------
-function {:existential true} {:inline} Assert() : bool
-{
- false
-}
-function {:existential true} {:inline} b1() : bool
-{
- false
-}
-function {:existential true} {:inline} b2(x: bool) : bool
-{
- false
-}
-function {:existential true} {:inline} b3(x: bool) : bool
-{
- false
-}
-function {:existential true} {:inline} b4(x: bool) : bool
-{
- false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd5.bpl --------------------
-function {:existential true} {:inline} b1(x: bool) : bool
-{
- !x
-}
-function {:existential true} {:inline} b2(x: bool) : bool
-{
- x
-}
-function {:existential true} {:inline} b3(x: bool) : bool
-{
- !x
-}
-function {:existential true} {:inline} b4(x: bool) : bool
-{
- x
-}
-function {:existential true} {:inline} b5() : bool
-{
- false
-}
-function {:existential true} {:inline} Assert() : bool
-{
- false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd6.bpl --------------------
-function {:existential true} {:inline} b1() : bool
-{
- true
-}
-function {:existential true} {:inline} b2() : bool
-{
- true
-}
-function {:existential true} {:inline} b3() : bool
-{
- true
-}
-function {:existential true} {:inline} b4() : bool
-{
- true
-}
-function {:existential true} {:inline} b5() : bool
-{
- true
-}
-function {:existential true} {:inline} b6() : bool
-{
- true
-}
-function {:existential true} {:inline} b7() : bool
-{
- true
-}
-function {:existential true} {:inline} b8() : bool
-{
- true
-}
-function {:existential true} {:inline} Assert() : bool
-{
- false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd7.bpl --------------------
-function {:existential true} {:inline} b1() : bool
-{
- false
-}
-function {:existential true} {:inline} b2() : bool
-{
- true
-}
-function {:existential true} {:inline} b3() : bool
-{
- true
-}
-function {:existential true} {:inline} Assert() : bool
-{
- false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd8.bpl --------------------
-function {:existential true} {:inline} b1() : bool
-{
- false
-}
-function {:existential true} {:inline} b2() : bool
-{
- true
-}
-function {:existential true} {:inline} b3() : bool
-{
- true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd10.bpl --------------------
-function {:existential true} {:inline} b1() : bool
-{
- true
-}
-function {:existential true} {:inline} b2() : bool
-{
- false
-}
-function {:existential true} {:inline} b3() : bool
-{
- true
-}
-function {:existential true} {:inline} Assert() : bool
-{
- true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd11.bpl --------------------
-function {:existential true} {:inline} Assert() : bool
-{
- true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- houd12.bpl --------------------
-function {:existential true} {:inline} Assert() : bool
-{
- false
-}
-function {:existential true} {:inline} b1() : bool
-{
- true
-}
-function {:existential true} {:inline} b2() : bool
-{
- false
-}
-function {:existential true} {:inline} b3() : bool
-{
- false
-}
-function {:existential true} {:inline} b4() : bool
-{
- false
-}
-function {:existential true} {:inline} b5() : bool
-{
- false
-}
-function {:existential true} {:inline} b6() : bool
-{
- true
-}
-function {:existential true} {:inline} b7() : bool
-{
- true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- fail1.bpl --------------------
-function {:existential true} {:inline} b1(x: bool) : bool
-{
- false
-}
-fail1.bpl(16,3): Error BP5001: This assertion might not hold.
-Execution trace:
- fail1.bpl(11,3): anon0
- fail1.bpl(12,11): anon4_Then
- fail1.bpl(16,3): anon3
-
-Boogie program verifier finished with 0 verified, 1 error
-.
--------------------- test1.bpl --------------------
-function {:existential true} {:inline} b0() : bool
-{
- false
-}
-function {:existential true} {:inline} b1() : bool
-{
- true
-}
-function {:existential true} {:inline} b2() : bool
-{
- true
-}
-function {:existential true} {:inline} Assert() : bool
-{
- false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- test2.bpl --------------------
-function {:existential true} {:inline} b0() : bool
-{
- false
-}
-function {:existential true} {:inline} b1() : bool
-{
- true
-}
-function {:existential true} {:inline} b2() : bool
-{
- true
-}
-function {:existential true} {:inline} Assert() : bool
-{
- false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- test7.bpl --------------------
-function {:existential true} {:inline} Assert() : bool
-{
- false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- test8.bpl --------------------
-function {:existential true} {:inline} Assert() : bool
-{
- false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- test9.bpl --------------------
-function {:existential true} {:inline} b1() : bool
-{
- true
-}
-function {:existential true} {:inline} b2() : bool
-{
- true
-}
-function {:existential true} {:inline} b3() : bool
-{
- true
-}
-function {:existential true} {:inline} b4() : bool
-{
- false
-}
-function {:existential true} {:inline} b5() : bool
-{
- true
-}
-function {:existential true} {:inline} b6() : bool
-{
- false
-}
-function {:existential true} {:inline} b7() : bool
-{
- true
-}
-function {:existential true} {:inline} b8() : bool
-{
- true
-}
-function {:existential true} {:inline} b9() : bool
-{
- true
-}
-function {:existential true} {:inline} b10() : bool
-{
- false
-}
-function {:existential true} {:inline} b11() : bool
-{
- true
-}
-function {:existential true} {:inline} b12() : bool
-{
- false
-}
-function {:existential true} {:inline} b13() : bool
-{
- true
-}
-function {:existential true} {:inline} b14() : bool
-{
- true
-}
-function {:existential true} {:inline} b15() : bool
-{
- true
-}
-function {:existential true} {:inline} b16() : bool
-{
- true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- test10.bpl --------------------
-function {:existential true} {:inline} b1() : bool
-{
- false
-}
-function {:existential true} {:inline} b2() : bool
-{
- false
-}
-function {:existential true} {:inline} b3() : bool
-{
- false
-}
-function {:existential true} {:inline} b4() : bool
-{
- false
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- pred1.bpl --------------------
-function {:existential true} {:inline} b0(x: bool, y: bool) : bool
-{
- x && !y
-}
-function {:existential true} {:inline} b1(x: bool, y: bool) : bool
-{
- (y || x) && (!x || !y)
-}
-function {:existential true} {:inline} b2(x: bool, y: bool) : bool
-{
- x && !y
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- pred2.bpl --------------------
-function {:existential true} {:inline} b0(x: bool) : bool
-{
- x
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- pred3.bpl --------------------
-function {:existential true} {:inline} b0(x: bool, y: bool) : bool
-{
- x && !y
-}
-function {:existential true} {:inline} b1(x: bool, y: bool) : bool
-{
- (y || x) && (!x || !y)
-}
-function {:existential true} {:inline} b2(x: bool, y: bool) : bool
-{
- x && !y
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- pred4.bpl --------------------
-function {:existential true} {:inline} b1(x: bool, y: bool) : bool
-{
- (y || x) && (!x || !y)
-}
-function {:existential true} {:absdomain "Intervals"} {:inline} b3(x: int) : bool
-{
- x >= 0 && x <= 0
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- pred5.bpl --------------------
-function {:existential true} {:inline} b1(x: bool) : bool
-{
- x
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- quant1.bpl --------------------
-function {:existential true} {:absdomain "IA[Intervals]"} {:inline} b1(x: int) : bool
-{
- x >= 0 && x <= 2
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- quant2.bpl --------------------
-function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
-{
- x >= 0 && x <= 1
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- quant3.bpl --------------------
-function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
-{
- x >= 0 && x <= 0
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- quant4.bpl --------------------
-function {:existential true} {:absdomain "IA[HoudiniConst]"} {:inline} b1() : bool
-{
- true
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
-.
--------------------- quant5.bpl --------------------
-function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
-{
- x >= 5 && x <= 5
-}
-
-Boogie program verifier finished with 1 verified, 0 errors
+ +-------------------- houd1.bpl -------------------- +function {:existential true} {:inline} b1(x: bool) : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- houd2.bpl -------------------- +function {:existential true} {:inline} Assert(x: bool) : bool +{ + true +} +function {:existential true} {:inline} b1(x: bool) : bool +{ + true +} +function {:existential true} {:inline} b2(x: bool) : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- houd3.bpl -------------------- +function {:existential true} {:inline} Assert(x: bool) : bool +{ + x +} +function {:existential true} {:inline} b1(x: bool) : bool +{ + true +} +function {:existential true} {:inline} b2(x: bool) : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- houd4.bpl -------------------- +function {:existential true} {:inline} Assert() : bool +{ + false +} +function {:existential true} {:inline} b1() : bool +{ + false +} +function {:existential true} {:inline} b2(x: bool) : bool +{ + false +} +function {:existential true} {:inline} b3(x: bool) : bool +{ + false +} +function {:existential true} {:inline} b4(x: bool) : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- houd5.bpl -------------------- +function {:existential true} {:inline} b1(x: bool) : bool +{ + !x +} +function {:existential true} {:inline} b2(x: bool) : bool +{ + x +} +function {:existential true} {:inline} b3(x: bool) : bool +{ + !x +} +function {:existential true} {:inline} b4(x: bool) : bool +{ + x +} +function {:existential true} {:inline} b5() : bool +{ + false +} +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- houd6.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} b3() : bool +{ + true +} +function {:existential true} {:inline} b4() : bool +{ + true +} +function {:existential true} {:inline} b5() : bool +{ + true +} +function {:existential true} {:inline} b6() : bool +{ + true +} +function {:existential true} {:inline} b7() : bool +{ + true +} +function {:existential true} {:inline} b8() : bool +{ + true +} +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- houd7.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + false +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} b3() : bool +{ + true +} +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- houd8.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + false +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} b3() : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- houd10.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + false +} +function {:existential true} {:inline} b3() : bool +{ + true +} +function {:existential true} {:inline} Assert() : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- houd11.bpl -------------------- +function {:existential true} {:inline} Assert() : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- houd12.bpl -------------------- +function {:existential true} {:inline} Assert() : bool +{ + false +} +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + false +} +function {:existential true} {:inline} b3() : bool +{ + false +} +function {:existential true} {:inline} b4() : bool +{ + false +} +function {:existential true} {:inline} b5() : bool +{ + false +} +function {:existential true} {:inline} b6() : bool +{ + true +} +function {:existential true} {:inline} b7() : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- fail1.bpl -------------------- +function {:existential true} {:inline} b1(x: bool) : bool +{ + false +} +fail1.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + fail1.bpl(11,3): anon0 + fail1.bpl(12,11): anon4_Then + fail1.bpl(16,3): anon3 + +Boogie program verifier finished with 0 verified, 1 error +. +-------------------- test1.bpl -------------------- +function {:existential true} {:inline} b0() : bool +{ + false +} +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- test2.bpl -------------------- +function {:existential true} {:inline} b0() : bool +{ + false +} +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- test7.bpl -------------------- +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- test8.bpl -------------------- +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- test9.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} b3() : bool +{ + true +} +function {:existential true} {:inline} b4() : bool +{ + false +} +function {:existential true} {:inline} b5() : bool +{ + true +} +function {:existential true} {:inline} b6() : bool +{ + false +} +function {:existential true} {:inline} b7() : bool +{ + true +} +function {:existential true} {:inline} b8() : bool +{ + true +} +function {:existential true} {:inline} b9() : bool +{ + true +} +function {:existential true} {:inline} b10() : bool +{ + false +} +function {:existential true} {:inline} b11() : bool +{ + true +} +function {:existential true} {:inline} b12() : bool +{ + false +} +function {:existential true} {:inline} b13() : bool +{ + true +} +function {:existential true} {:inline} b14() : bool +{ + true +} +function {:existential true} {:inline} b15() : bool +{ + true +} +function {:existential true} {:inline} b16() : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- test10.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + false +} +function {:existential true} {:inline} b2() : bool +{ + false +} +function {:existential true} {:inline} b3() : bool +{ + false +} +function {:existential true} {:inline} b4() : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- pred1.bpl -------------------- +function {:existential true} {:inline} b0(x: bool, y: bool) : bool +{ + x && !y +} +function {:existential true} {:inline} b1(x: bool, y: bool) : bool +{ + (y || x) && (!x || !y) +} +function {:existential true} {:inline} b2(x: bool, y: bool) : bool +{ + x && !y +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- pred2.bpl -------------------- +function {:existential true} {:inline} b0(x: bool) : bool +{ + x +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- pred3.bpl -------------------- +function {:existential true} {:inline} b0(x: bool, y: bool) : bool +{ + x && !y +} +function {:existential true} {:inline} b1(x: bool, y: bool) : bool +{ + (y || x) && (!x || !y) +} +function {:existential true} {:inline} b2(x: bool, y: bool) : bool +{ + x && !y +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- pred4.bpl -------------------- +function {:existential true} {:inline} b1(x: bool, y: bool) : bool +{ + (y || x) && (!x || !y) +} +function {:existential true} {:absdomain "Intervals"} {:inline} b3(x: int) : bool +{ + x >= 0 && x <= 0 +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- pred5.bpl -------------------- +function {:existential true} {:inline} b1(x: bool) : bool +{ + x +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- quant1.bpl -------------------- +function {:existential true} {:absdomain "IA[Intervals]"} {:inline} b1(x: int) : bool +{ + x >= 0 && x <= 2 +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- quant2.bpl -------------------- +function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool +{ + x >= 0 && x <= 1 +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- quant3.bpl -------------------- +function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool +{ + x >= 0 && x <= 0 +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- quant4.bpl -------------------- +function {:existential true} {:absdomain "IA[HoudiniConst]"} {:inline} b1() : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- quant5.bpl -------------------- +function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool +{ + x >= 5 && x <= 5 +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/f1.bpl b/Test/AbsHoudini/f1.bpl index e5ed85ef..b7ee9011 100644 --- a/Test/AbsHoudini/f1.bpl +++ b/Test/AbsHoudini/f1.bpl @@ -1,32 +1,32 @@ -var g: int;
-
-procedure {:entrypoint} main()
- modifies g;
-{
- var x: int;
- var c: bool;
-
- g := 1;
-
- if(c) {
- g := g + 1;
- } else {
- g := 3;
- }
-
- call foo();
-
- if(old(g) == 0) { g := 1; }
-}
-
-procedure foo()
- modifies g;
-{
- g := g + 1;
-}
-
-procedure {:template} summaryTemplate();
- ensures {:post} g == old(g) + 1;
- ensures {:post} g == old(g) + 2;
- ensures {:post} g == old(g) + 3;
- ensures {:pre} old(g) == 0;
+var g: int; + +procedure {:entrypoint} main() + modifies g; +{ + var x: int; + var c: bool; + + g := 1; + + if(c) { + g := g + 1; + } else { + g := 3; + } + + call foo(); + + if(old(g) == 0) { g := 1; } +} + +procedure foo() + modifies g; +{ + g := g + 1; +} + +procedure {:template} summaryTemplate(); + ensures {:post} g == old(g) + 1; + ensures {:post} g == old(g) + 2; + ensures {:post} g == old(g) + 3; + ensures {:pre} old(g) == 0; diff --git a/Test/AbsHoudini/fail1.bpl b/Test/AbsHoudini/fail1.bpl index 02bcb8d3..4605c7e9 100644 --- a/Test/AbsHoudini/fail1.bpl +++ b/Test/AbsHoudini/fail1.bpl @@ -1,18 +1,18 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b1(x: bool) : bool;
-
-var myVar: int;
-
-procedure foo (i:int)
-modifies myVar;
-ensures b1(myVar>0);
-{
- if (i>0) {
- myVar := 5;
- } else {
- myVar := 0;
- }
- assert false;
-}
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b1(x: bool) : bool; + +var myVar: int; + +procedure foo (i:int) +modifies myVar; +ensures b1(myVar>0); +{ + if (i>0) { + myVar := 5; + } else { + myVar := 0; + } + assert false; +} + diff --git a/Test/AbsHoudini/houd1.bpl b/Test/AbsHoudini/houd1.bpl index 0bd4831a..eeab11aa 100644 --- a/Test/AbsHoudini/houd1.bpl +++ b/Test/AbsHoudini/houd1.bpl @@ -1,19 +1,19 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b1(x: bool) : bool;
-
-var myVar: int;
-
-procedure foo (i:int)
-modifies myVar;
-// comment
-ensures b1(myVar>0);
-{
- if (i>0) {
- myVar := 5;
- } else {
- myVar := 0;
- }
-}
-
-// expected end assigment: b1(x) = true
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b1(x: bool) : bool; + +var myVar: int; + +procedure foo (i:int) +modifies myVar; +// comment +ensures b1(myVar>0); +{ + if (i>0) { + myVar := 5; + } else { + myVar := 0; + } +} + +// expected end assigment: b1(x) = true diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl index 5a0942cc..02dd91c1 100644 --- a/Test/AbsHoudini/houd10.bpl +++ b/Test/AbsHoudini/houd10.bpl @@ -1,24 +1,24 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b1():bool;
-function {:existential true} b2():bool;
-function {:existential true} b3():bool;
-function {:existential true} Assert(): bool;
-var fooVar: int;
-var xVar: int;
-
-procedure foo()
-modifies fooVar;
-modifies xVar;
-ensures b1() || fooVar==0;
-ensures b3() || xVar<0;
-{
- fooVar:=5;
- call bar();
-}
-
-procedure bar();
-modifies xVar;
-requires Assert() || fooVar!=5;
-
-// expected assigment: Assert->true,b1->True,b2->false,b3->True
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b1():bool; +function {:existential true} b2():bool; +function {:existential true} b3():bool; +function {:existential true} Assert(): bool; +var fooVar: int; +var xVar: int; + +procedure foo() +modifies fooVar; +modifies xVar; +ensures b1() || fooVar==0; +ensures b3() || xVar<0; +{ + fooVar:=5; + call bar(); +} + +procedure bar(); +modifies xVar; +requires Assert() || fooVar!=5; + +// expected assigment: Assert->true,b1->True,b2->false,b3->True diff --git a/Test/AbsHoudini/houd11.bpl b/Test/AbsHoudini/houd11.bpl index 638d8ec2..a493574d 100644 --- a/Test/AbsHoudini/houd11.bpl +++ b/Test/AbsHoudini/houd11.bpl @@ -1,15 +1,15 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} Assert() : bool;
-
-var fooVar: int;
-
-procedure foo()
-modifies fooVar;
-{
- fooVar:=5;
- assert Assert() || (fooVar==4);
- assert Assert() || (fooVar==3);
-}
-
-// expected assigment: Assert -> true
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} Assert() : bool; + +var fooVar: int; + +procedure foo() +modifies fooVar; +{ + fooVar:=5; + assert Assert() || (fooVar==4); + assert Assert() || (fooVar==3); +} + +// expected assigment: Assert -> true diff --git a/Test/AbsHoudini/houd12.bpl b/Test/AbsHoudini/houd12.bpl index 12727d65..434cdc5b 100644 --- a/Test/AbsHoudini/houd12.bpl +++ b/Test/AbsHoudini/houd12.bpl @@ -1,60 +1,60 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Example to test candidate annotations on loops
-
-function {:existential true} Assert(): bool;
-function {:existential true} b1():bool;
-function {:existential true} b2():bool;
-function {:existential true} b3():bool;
-function {:existential true} b4():bool;
-function {:existential true} b5():bool;
-function {:existential true} b6():bool;
-function {:existential true} b7():bool;
-
-var x: int;
-var y: int;
-
-
-procedure foo()
-modifies x;
-modifies y;
-ensures (b4() || x == 0);
-ensures (b5() || y == 10);
-ensures (b6() || x == 10);
-ensures (b7() || y == 11);
-
-{
- x := 10;
- y := 0;
-
- goto Head;
-
-Head:
-
- //loop invariants
- assert (b1() || x < 0);
- assert (b2() || x >= 0);
- assert (b3() || x + y == 10);
- goto Body, Exit;
-
-Body:
- assume x > 0;
- x := x - 1;
- y := y + 1;
-
-
- goto Head;
-
-Exit:
- assume !(x > 0);
- return;
-}
-
-// expected assigment: Assert -> false, b1->true,b2->false,b3->false,b4->false, b5->false, b6->true,b7->true
-
-
-
-
-
-
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// Example to test candidate annotations on loops + +function {:existential true} Assert(): bool; +function {:existential true} b1():bool; +function {:existential true} b2():bool; +function {:existential true} b3():bool; +function {:existential true} b4():bool; +function {:existential true} b5():bool; +function {:existential true} b6():bool; +function {:existential true} b7():bool; + +var x: int; +var y: int; + + +procedure foo() +modifies x; +modifies y; +ensures (b4() || x == 0); +ensures (b5() || y == 10); +ensures (b6() || x == 10); +ensures (b7() || y == 11); + +{ + x := 10; + y := 0; + + goto Head; + +Head: + + //loop invariants + assert (b1() || x < 0); + assert (b2() || x >= 0); + assert (b3() || x + y == 10); + goto Body, Exit; + +Body: + assume x > 0; + x := x - 1; + y := y + 1; + + + goto Head; + +Exit: + assume !(x > 0); + return; +} + +// expected assigment: Assert -> false, b1->true,b2->false,b3->false,b4->false, b5->false, b6->true,b7->true + + + + + + + diff --git a/Test/AbsHoudini/houd2.bpl b/Test/AbsHoudini/houd2.bpl index 97a73464..5fce886e 100644 --- a/Test/AbsHoudini/houd2.bpl +++ b/Test/AbsHoudini/houd2.bpl @@ -1,29 +1,29 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} Assert(x:bool) : bool;
-function {:existential true} b1 (x:bool):bool;
-function {:existential true} b2 (x:bool):bool;
-
-
-var myVar: int;
-
-procedure bar(i:int)
-modifies myVar;
-ensures Assert(myVar>0);
-{
- call foo(5);
-}
-
-procedure foo (i:int)
-modifies myVar;
-ensures b1(myVar>0);
-ensures Assert(myVar!=-1);
-{
- if (i>0) {
- myVar := 5;
- } else {
- myVar := 0;
- }
-}
-
-// expected end assigment: Assert(x) = true, b1(x) = true, b2(x) = false
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} Assert(x:bool) : bool; +function {:existential true} b1 (x:bool):bool; +function {:existential true} b2 (x:bool):bool; + + +var myVar: int; + +procedure bar(i:int) +modifies myVar; +ensures Assert(myVar>0); +{ + call foo(5); +} + +procedure foo (i:int) +modifies myVar; +ensures b1(myVar>0); +ensures Assert(myVar!=-1); +{ + if (i>0) { + myVar := 5; + } else { + myVar := 0; + } +} + +// expected end assigment: Assert(x) = true, b1(x) = true, b2(x) = false diff --git a/Test/AbsHoudini/houd3.bpl b/Test/AbsHoudini/houd3.bpl index 178c0e36..3a9f87c3 100644 --- a/Test/AbsHoudini/houd3.bpl +++ b/Test/AbsHoudini/houd3.bpl @@ -1,29 +1,29 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} Assert(x: bool) : bool;
-function {:existential true} b1(x: bool) : bool;
-function {:existential true} b2(x: bool) : bool;
-
-
-var myVar: int;
-
-procedure bar(i:int)
-modifies myVar;
-ensures b2(myVar>0);
-{
- call foo(5);
-}
-
-procedure foo (i:int)
-modifies myVar;
-ensures b1(myVar>0);
-ensures Assert(myVar!=-1);
-{
- if (i>0) {
- myVar := 5;
- } else {
- myVar := 0;
- }
-}
-
-// expected end assigment: Assert(x) = x, b1(x) = True, b2(x) = True
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} Assert(x: bool) : bool; +function {:existential true} b1(x: bool) : bool; +function {:existential true} b2(x: bool) : bool; + + +var myVar: int; + +procedure bar(i:int) +modifies myVar; +ensures b2(myVar>0); +{ + call foo(5); +} + +procedure foo (i:int) +modifies myVar; +ensures b1(myVar>0); +ensures Assert(myVar!=-1); +{ + if (i>0) { + myVar := 5; + } else { + myVar := 0; + } +} + +// expected end assigment: Assert(x) = x, b1(x) = True, b2(x) = True diff --git a/Test/AbsHoudini/houd4.bpl b/Test/AbsHoudini/houd4.bpl index 3268ce12..8639726a 100644 --- a/Test/AbsHoudini/houd4.bpl +++ b/Test/AbsHoudini/houd4.bpl @@ -1,29 +1,29 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} Assert() : bool;
-function {:existential true} b1():bool;
-function {:existential true} b2(x:bool):bool;
-function {:existential true} b3(x:bool):bool;
-function {:existential true} b4(x:bool):bool;
-
-var array:[int]int;
-
-procedure foo (i:int)
-requires b2(i > 0);
-ensures b3(array[i] > 0);
-modifies array;
-ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
-{
- array[i] := 2 * i;
-}
-
-procedure bar (j:int) returns (result:int)
-requires b4(j > 0);
-modifies array;
-ensures Assert() || (forall x:int :: {array[x]} (!b1() && x == j) || array[x] == old(array)[x]);
-{
- call foo(j);
- result := array[j];
-}
-
-// expected assignment: Assert = false, b1(x) = false, b2(x) = false, b3(x) = false, b4(x) = false
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} Assert() : bool; +function {:existential true} b1():bool; +function {:existential true} b2(x:bool):bool; +function {:existential true} b3(x:bool):bool; +function {:existential true} b4(x:bool):bool; + +var array:[int]int; + +procedure foo (i:int) +requires b2(i > 0); +ensures b3(array[i] > 0); +modifies array; +ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]); +{ + array[i] := 2 * i; +} + +procedure bar (j:int) returns (result:int) +requires b4(j > 0); +modifies array; +ensures Assert() || (forall x:int :: {array[x]} (!b1() && x == j) || array[x] == old(array)[x]); +{ + call foo(j); + result := array[j]; +} + +// expected assignment: Assert = false, b1(x) = false, b2(x) = false, b3(x) = false, b4(x) = false diff --git a/Test/AbsHoudini/houd5.bpl b/Test/AbsHoudini/houd5.bpl index 9a4c274b..71045f23 100644 --- a/Test/AbsHoudini/houd5.bpl +++ b/Test/AbsHoudini/houd5.bpl @@ -1,31 +1,31 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b1(x:bool):bool;
-function {:existential true} b2(x:bool):bool;
-function {:existential true} b3(x:bool):bool;
-function {:existential true} b4(x:bool):bool;
-function {:existential true} b5():bool;
-function {:existential true} Assert():bool;
-
-var array:[int]int;
-
-procedure foo (i:int)
-requires b1(i == 0);
-requires b2(i > 0);
-requires b3(i < 0);
-ensures b4(array[i] > 0);
-modifies array;
-ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
-{
- array[i] := 2 * i;
-}
-
-procedure bar (j:int) returns (result:int)
-requires b5() || (j > 0);
-modifies array;
-{
- call foo(j);
- result := array[j];
-}
-
-// expected assigment: assert = false, b1(x) = !x, b2(x) = x, b3(x) = !x, b4(x) = x, b5() = false
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b1(x:bool):bool; +function {:existential true} b2(x:bool):bool; +function {:existential true} b3(x:bool):bool; +function {:existential true} b4(x:bool):bool; +function {:existential true} b5():bool; +function {:existential true} Assert():bool; + +var array:[int]int; + +procedure foo (i:int) +requires b1(i == 0); +requires b2(i > 0); +requires b3(i < 0); +ensures b4(array[i] > 0); +modifies array; +ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]); +{ + array[i] := 2 * i; +} + +procedure bar (j:int) returns (result:int) +requires b5() || (j > 0); +modifies array; +{ + call foo(j); + result := array[j]; +} + +// expected assigment: assert = false, b1(x) = !x, b2(x) = x, b3(x) = !x, b4(x) = x, b5() = false diff --git a/Test/AbsHoudini/houd6.bpl b/Test/AbsHoudini/houd6.bpl index 4d9cc9e8..4279e4ce 100644 --- a/Test/AbsHoudini/houd6.bpl +++ b/Test/AbsHoudini/houd6.bpl @@ -1,46 +1,46 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b1():bool;
-function {:existential true} b2():bool;
-function {:existential true} b3():bool;
-function {:existential true} b4():bool;
-function {:existential true} b5():bool;
-function {:existential true} b6():bool;
-function {:existential true} b7():bool;
-function {:existential true} b8():bool;
-function {:existential true} Assert(): bool;
-
-var array:[int]int;
-
-procedure foo (i:int)
-requires b6() || i < 0;
-requires b5() || i == 0;
-requires b2() || i > 0;
-ensures b3() || array[i] > 0;
-modifies array;
-ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
-{
- array[i] := 2 * i;
-}
-
-procedure bar (j:int) returns (result:int)
-requires b8() || j < 0;
-requires b7() || j == 0;
-requires b4() || j > 0;
-modifies array;
-ensures Assert() || (forall x:int :: {array[x]} (x == j) || array[x] == old(array)[x]);
-ensures b1() || array[j] == old(array)[j];
-{
- call foo(j);
- result := array[j];
-}
-
-var p:int;
-
-procedure main() returns (result: int)
-modifies array;
-{
- call result:= bar(p);
-}
-
-// expected assigment: Assert -> false, bi->true forall i
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b1():bool; +function {:existential true} b2():bool; +function {:existential true} b3():bool; +function {:existential true} b4():bool; +function {:existential true} b5():bool; +function {:existential true} b6():bool; +function {:existential true} b7():bool; +function {:existential true} b8():bool; +function {:existential true} Assert(): bool; + +var array:[int]int; + +procedure foo (i:int) +requires b6() || i < 0; +requires b5() || i == 0; +requires b2() || i > 0; +ensures b3() || array[i] > 0; +modifies array; +ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]); +{ + array[i] := 2 * i; +} + +procedure bar (j:int) returns (result:int) +requires b8() || j < 0; +requires b7() || j == 0; +requires b4() || j > 0; +modifies array; +ensures Assert() || (forall x:int :: {array[x]} (x == j) || array[x] == old(array)[x]); +ensures b1() || array[j] == old(array)[j]; +{ + call foo(j); + result := array[j]; +} + +var p:int; + +procedure main() returns (result: int) +modifies array; +{ + call result:= bar(p); +} + +// expected assigment: Assert -> false, bi->true forall i diff --git a/Test/AbsHoudini/houd7.bpl b/Test/AbsHoudini/houd7.bpl index 4035755c..9272fa3c 100644 --- a/Test/AbsHoudini/houd7.bpl +++ b/Test/AbsHoudini/houd7.bpl @@ -1,37 +1,37 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b1():bool;
-function {:existential true} b2():bool;
-function {:existential true} b3():bool;
-function {:existential true} Assert(): bool;
-var myVar: int;
-
-procedure foo(i:int)
-requires b1() || i>0;
-requires b2() || i==0;
-requires b3() || i<0;
-modifies myVar;
-ensures Assert() || myVar>0;
-{
- myVar:=5;
-}
-
-procedure bar(i:int)
-modifies myVar;
-{
- call foo(5);
-}
-// expected outcome: Correct
-// expected Assigment: Assert = false, b1->false,b2->true,b3->true
-
-
-
-
-
-
-
-
-
-
-
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b1():bool; +function {:existential true} b2():bool; +function {:existential true} b3():bool; +function {:existential true} Assert(): bool; +var myVar: int; + +procedure foo(i:int) +requires b1() || i>0; +requires b2() || i==0; +requires b3() || i<0; +modifies myVar; +ensures Assert() || myVar>0; +{ + myVar:=5; +} + +procedure bar(i:int) +modifies myVar; +{ + call foo(5); +} +// expected outcome: Correct +// expected Assigment: Assert = false, b1->false,b2->true,b3->true + + + + + + + + + + + + diff --git a/Test/AbsHoudini/houd8.bpl b/Test/AbsHoudini/houd8.bpl index dff155aa..7fdf514e 100644 --- a/Test/AbsHoudini/houd8.bpl +++ b/Test/AbsHoudini/houd8.bpl @@ -1,31 +1,31 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b1():bool;
-function {:existential true} b2():bool;
-function {:existential true} b3():bool;
-
-var myVar: int;
-
-procedure foo(i:int)
-modifies myVar;
-ensures b1() || myVar>0;
-ensures b2() || myVar==0;
-ensures b3() || myVar<0;
-{
- myVar:=5;
-}
-
-// expected assigment: b1->false,b2->true,b3->true
-
-
-
-
-
-
-
-
-
-
-
-
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b1():bool; +function {:existential true} b2():bool; +function {:existential true} b3():bool; + +var myVar: int; + +procedure foo(i:int) +modifies myVar; +ensures b1() || myVar>0; +ensures b2() || myVar==0; +ensures b3() || myVar<0; +{ + myVar:=5; +} + +// expected assigment: b1->false,b2->true,b3->true + + + + + + + + + + + + + diff --git a/Test/AbsHoudini/imp1.bpl b/Test/AbsHoudini/imp1.bpl index 29cbf567..09be87e7 100644 --- a/Test/AbsHoudini/imp1.bpl +++ b/Test/AbsHoudini/imp1.bpl @@ -1,21 +1,21 @@ -function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool;
-function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool;
-
-var x: int;
-var flag: bool;
-
-procedure foo ()
- modifies x, flag;
- ensures b1(flag, x == 0);
-{
- flag := true;
- x := 0;
-}
-
-procedure bar()
- modifies x, flag;
- ensures b2(flag, x == 0);
-{
- flag := false;
- x := 0;
-}
+function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool; +function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool; + +var x: int; +var flag: bool; + +procedure foo () + modifies x, flag; + ensures b1(flag, x == 0); +{ + flag := true; + x := 0; +} + +procedure bar() + modifies x, flag; + ensures b2(flag, x == 0); +{ + flag := false; + x := 0; +} diff --git a/Test/AbsHoudini/int1.bpl b/Test/AbsHoudini/int1.bpl index 0ee0f1b9..eb4e6b51 100644 --- a/Test/AbsHoudini/int1.bpl +++ b/Test/AbsHoudini/int1.bpl @@ -1,26 +1,26 @@ -function {:existential true} b0(x:int): bool;
-function {:existential true} b1(x:int): bool;
-
-var g: int;
-
-procedure foo()
-modifies g;
-requires b0(g);
-ensures b1(g);
-{
- if(*) {
- g := g + 1;
- call foo();
- }
-}
-
-procedure main()
-modifies g;
-{
- g := 0;
- if(*) { g := 5; }
- call foo();
-}
-
-
-// Expected: b0(x) = [0,\infty], b1(x) = [0, \infty]
+function {:existential true} b0(x:int): bool; +function {:existential true} b1(x:int): bool; + +var g: int; + +procedure foo() +modifies g; +requires b0(g); +ensures b1(g); +{ + if(*) { + g := g + 1; + call foo(); + } +} + +procedure main() +modifies g; +{ + g := 0; + if(*) { g := 5; } + call foo(); +} + + +// Expected: b0(x) = [0,\infty], b1(x) = [0, \infty] diff --git a/Test/AbsHoudini/multi.bpl b/Test/AbsHoudini/multi.bpl index a33817ac..e53bb075 100644 --- a/Test/AbsHoudini/multi.bpl +++ b/Test/AbsHoudini/multi.bpl @@ -1,67 +1,67 @@ -function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool;
-function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool;
-function {:existential true} {:absdomain "PowDomain"} b3(x1: int) : bool;
-function {:existential true} {:absdomain "PowDomain"} b4(x1: bv32) : bool;
-function {:existential true} {:absdomain "EqualitiesDomain"} b5(x: int, y: int, z: int, w:int) : bool;
-
-function {:builtin "bvslt"} BV_SLT(x: bv32, y: bv32) : bool;
-
-var x: int;
-var flag: bool;
-
-// Test implication domain
-procedure foo ()
- modifies x, flag;
-{
- flag := true;
- x := 0;
- assert b1(flag, x == 0);
- flag := false;
- assert b2(flag, x == 0);
-}
-
-// Test for PowDomain(int)
-procedure bar1 ()
- modifies x, flag;
-{
- x := 2;
- if(*) { x := 16; }
- assert b3(x);
-}
-
-// Test for PowDomain(bv32)
-procedure bar2 ()
- modifies x, flag;
-{
- var s: bv32;
-
- s := 2bv32;
- if(*) { s := 16bv32; }
- assert b4(s);
-}
-
-// Test for EqualitiesDomain
-procedure baz ()
- modifies x, flag;
-{
- var y: int;
- var z: int;
- var w: int;
-
- assume x == y;
- assume x == z;
-
- if(*) {
- x := x + 1;
- y := y + 1;
- } else {
- x := x + 2;
- y := y + 2;
- }
-
- assume x == w;
-
- assert b5(x,y,z,w);
-}
-
-
+function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool; +function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool; +function {:existential true} {:absdomain "PowDomain"} b3(x1: int) : bool; +function {:existential true} {:absdomain "PowDomain"} b4(x1: bv32) : bool; +function {:existential true} {:absdomain "EqualitiesDomain"} b5(x: int, y: int, z: int, w:int) : bool; + +function {:builtin "bvslt"} BV_SLT(x: bv32, y: bv32) : bool; + +var x: int; +var flag: bool; + +// Test implication domain +procedure foo () + modifies x, flag; +{ + flag := true; + x := 0; + assert b1(flag, x == 0); + flag := false; + assert b2(flag, x == 0); +} + +// Test for PowDomain(int) +procedure bar1 () + modifies x, flag; +{ + x := 2; + if(*) { x := 16; } + assert b3(x); +} + +// Test for PowDomain(bv32) +procedure bar2 () + modifies x, flag; +{ + var s: bv32; + + s := 2bv32; + if(*) { s := 16bv32; } + assert b4(s); +} + +// Test for EqualitiesDomain +procedure baz () + modifies x, flag; +{ + var y: int; + var z: int; + var w: int; + + assume x == y; + assume x == z; + + if(*) { + x := x + 1; + y := y + 1; + } else { + x := x + 2; + y := y + 2; + } + + assume x == w; + + assert b5(x,y,z,w); +} + + diff --git a/Test/AbsHoudini/pred1.bpl b/Test/AbsHoudini/pred1.bpl index 4db4810e..51c310cc 100644 --- a/Test/AbsHoudini/pred1.bpl +++ b/Test/AbsHoudini/pred1.bpl @@ -1,25 +1,25 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b0(x:bool, y:bool): bool;
-function {:existential true} b1(x:bool, y:bool): bool;
-function {:existential true} b2(x:bool, y:bool): bool;
-
-var g: int;
-
-procedure main()
-modifies g;
-ensures b0(g == 0, g == 5);
-{
- g := 0;
- if(*) { g := 5; }
- call foo();
-}
-
-procedure foo()
- modifies g;
- requires b1(g == 0, g == 5);
- ensures b2(g == 0, g == 5);
-{
- assume g != 5;
-}
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b0(x:bool, y:bool): bool; +function {:existential true} b1(x:bool, y:bool): bool; +function {:existential true} b2(x:bool, y:bool): bool; + +var g: int; + +procedure main() +modifies g; +ensures b0(g == 0, g == 5); +{ + g := 0; + if(*) { g := 5; } + call foo(); +} + +procedure foo() + modifies g; + requires b1(g == 0, g == 5); + ensures b2(g == 0, g == 5); +{ + assume g != 5; +} + diff --git a/Test/AbsHoudini/pred2.bpl b/Test/AbsHoudini/pred2.bpl index c9ac3f74..f34bf5d6 100644 --- a/Test/AbsHoudini/pred2.bpl +++ b/Test/AbsHoudini/pred2.bpl @@ -1,14 +1,14 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b0(x:bool): bool;
-
-var g: int;
-
-procedure main()
-modifies g;
-ensures b0(g == old(g));
-{
- if(*) { g := 5; }
- assume g != 5;
-}
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b0(x:bool): bool; + +var g: int; + +procedure main() +modifies g; +ensures b0(g == old(g)); +{ + if(*) { g := 5; } + assume g != 5; +} + diff --git a/Test/AbsHoudini/pred3.bpl b/Test/AbsHoudini/pred3.bpl index 38f42088..ef76a073 100644 --- a/Test/AbsHoudini/pred3.bpl +++ b/Test/AbsHoudini/pred3.bpl @@ -1,26 +1,26 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b0(x:bool, y:bool): bool;
-function {:existential true} b1(x:bool, y:bool): bool;
-function {:existential true} b2(x:bool, y:bool): bool;
-
-var g: int;
-
-procedure main()
-modifies g;
-ensures b0(g == 0, g == 5);
-{
- assume 0 == old(g) || 1 == old(g);
- g := 0;
- if(*) { g := 5; }
- call foo();
-}
-
-procedure foo()
- modifies g;
- requires b1(g == 0, g == 5);
- ensures b2(old(g) == 0, old(g) == 5);
-{
- assume g != 5;
-}
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b0(x:bool, y:bool): bool; +function {:existential true} b1(x:bool, y:bool): bool; +function {:existential true} b2(x:bool, y:bool): bool; + +var g: int; + +procedure main() +modifies g; +ensures b0(g == 0, g == 5); +{ + assume 0 == old(g) || 1 == old(g); + g := 0; + if(*) { g := 5; } + call foo(); +} + +procedure foo() + modifies g; + requires b1(g == 0, g == 5); + ensures b2(old(g) == 0, old(g) == 5); +{ + assume g != 5; +} + diff --git a/Test/AbsHoudini/pred4.bpl b/Test/AbsHoudini/pred4.bpl index 06e504e2..be9fd1f5 100644 --- a/Test/AbsHoudini/pred4.bpl +++ b/Test/AbsHoudini/pred4.bpl @@ -1,23 +1,23 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b1(x:bool, y:bool): bool;
-function {:existential true} {:absdomain "Intervals"} b3(x:int): bool;
-
-var g: int;
-
-procedure main()
-modifies g;
-{
- g := 0;
- if(*) { g := 5; }
- call foo();
-}
-
-procedure foo()
- modifies g;
- requires b1(g == 0, g == 5);
- ensures b3(g);
-{
- assume g != 5;
-}
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b1(x:bool, y:bool): bool; +function {:existential true} {:absdomain "Intervals"} b3(x:int): bool; + +var g: int; + +procedure main() +modifies g; +{ + g := 0; + if(*) { g := 5; } + call foo(); +} + +procedure foo() + modifies g; + requires b1(g == 0, g == 5); + ensures b3(g); +{ + assume g != 5; +} + diff --git a/Test/AbsHoudini/pred5.bpl b/Test/AbsHoudini/pred5.bpl index 1c96fe4d..ee270b15 100644 --- a/Test/AbsHoudini/pred5.bpl +++ b/Test/AbsHoudini/pred5.bpl @@ -1,26 +1,26 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} b1(x: bool) : bool;
-
-procedure main()
-{
- var i: int;
- var x: int;
- var arr: [int] int;
-
- i := 0;
-
- while(*)
- invariant b1((i >= 0) && (forall j: int :: (0 <= j && j < i) ==> arr[j] == 0));
- {
- havoc x;
- assume x == 0;
-
- arr[i] := x;
- i := i + 1;
- }
-
- havoc x;
- assume x >= 0 && x < i;
- assert b1(arr[x] == 0);
-}
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} b1(x: bool) : bool; + +procedure main() +{ + var i: int; + var x: int; + var arr: [int] int; + + i := 0; + + while(*) + invariant b1((i >= 0) && (forall j: int :: (0 <= j && j < i) ==> arr[j] == 0)); + { + havoc x; + assume x == 0; + + arr[i] := x; + i := i + 1; + } + + havoc x; + assume x >= 0 && x < i; + assert b1(arr[x] == 0); +} diff --git a/Test/AbsHoudini/quant1.bpl b/Test/AbsHoudini/quant1.bpl index c3a8814c..d4f2b76b 100644 --- a/Test/AbsHoudini/quant1.bpl +++ b/Test/AbsHoudini/quant1.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} {:absdomain "IA[Intervals]"} b1(x: int) : bool;
-
-procedure foo ()
-{
- assert (forall x: int :: (0 <= x && x <= 2) ==> b1(x));
-}
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} {:absdomain "IA[Intervals]"} b1(x: int) : bool; + +procedure foo () +{ + assert (forall x: int :: (0 <= x && x <= 2) ==> b1(x)); +} + diff --git a/Test/AbsHoudini/quant2.bpl b/Test/AbsHoudini/quant2.bpl index 1091155b..08fafae9 100644 --- a/Test/AbsHoudini/quant2.bpl +++ b/Test/AbsHoudini/quant2.bpl @@ -1,26 +1,26 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
-
-procedure main()
-{
- var i: int;
- var x: int;
- var arr: [int] int;
-
- i := 0;
-
- while(*)
- invariant (i >= 0) && (forall j: int :: (0 <= j && j < i) ==> b1(arr[j]));
- {
- havoc x;
- assume x == 0 || x == 1;
-
- arr[i] := x;
- i := i + 1;
- }
-
- havoc x;
- assume x >= 0 && x < i;
- assert arr[x] == 0 || arr[x] == 1;
-}
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool; + +procedure main() +{ + var i: int; + var x: int; + var arr: [int] int; + + i := 0; + + while(*) + invariant (i >= 0) && (forall j: int :: (0 <= j && j < i) ==> b1(arr[j])); + { + havoc x; + assume x == 0 || x == 1; + + arr[i] := x; + i := i + 1; + } + + havoc x; + assume x >= 0 && x < i; + assert arr[x] == 0 || arr[x] == 1; +} diff --git a/Test/AbsHoudini/quant3.bpl b/Test/AbsHoudini/quant3.bpl index 951639ff..4a87404f 100644 --- a/Test/AbsHoudini/quant3.bpl +++ b/Test/AbsHoudini/quant3.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
-
-procedure foo ()
-{
- assert (exists x: int :: (0 <= x && x <= 2) && b1(x));
-}
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool; + +procedure foo () +{ + assert (exists x: int :: (0 <= x && x <= 2) && b1(x)); +} + diff --git a/Test/AbsHoudini/quant4.bpl b/Test/AbsHoudini/quant4.bpl index ac24d7ce..38029355 100644 --- a/Test/AbsHoudini/quant4.bpl +++ b/Test/AbsHoudini/quant4.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} {:absdomain "IA[HoudiniConst]"} b1() : bool;
-
-procedure foo ()
-{
- assert (exists x: int :: (0 <= x && x <= 2) && b1());
-}
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} {:absdomain "IA[HoudiniConst]"} b1() : bool; + +procedure foo () +{ + assert (exists x: int :: (0 <= x && x <= 2) && b1()); +} + diff --git a/Test/AbsHoudini/quant5.bpl b/Test/AbsHoudini/quant5.bpl index d511e9ac..fb73a137 100644 --- a/Test/AbsHoudini/quant5.bpl +++ b/Test/AbsHoudini/quant5.bpl @@ -1,13 +1,13 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
-
-procedure foo ()
-{
- var arr: [int] int;
- assume (forall x: int :: arr[x] == 0);
- arr[5] := 1;
-
- assert (exists x: int :: arr[x] == 1 && b1(x));
-}
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool; + +procedure foo () +{ + var arr: [int] int; + assume (forall x: int :: arr[x] == 0); + arr[5] := 1; + + assert (exists x: int :: arr[x] == 1 && b1(x)); +} + diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat index 4d70be0e..3053f5fb 100644 --- a/Test/AbsHoudini/runtest.bat +++ b/Test/AbsHoudini/runtest.bat @@ -1,28 +1,28 @@ -@echo off
-setlocal
-
-set BGEXE=..\..\Binaries\Boogie.exe
-
-for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd10.bpl houd11.bpl houd12.bpl fail1.bpl) do (
- echo.
- echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:IA[ConstantProp] %%f
-)
-
-for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
- echo .
- echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:IA[ConstantProp] %%f
-)
-
-for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl pred5.bpl) do (
- echo .
- echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:PredicateAbs %%f
-)
-
-for %%f in (quant1.bpl quant2.bpl quant3.bpl quant4.bpl quant5.bpl) do (
- echo .
- echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:HoudiniConst /z3opt:MBQI=true %%f
-)
+@echo off +setlocal + +set BGEXE=..\..\Binaries\Boogie.exe + +for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd10.bpl houd11.bpl houd12.bpl fail1.bpl) do ( + echo. + echo -------------------- %%f -------------------- + %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:IA[ConstantProp] %%f +) + +for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do ( + echo . + echo -------------------- %%f -------------------- + %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:IA[ConstantProp] %%f +) + +for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl pred5.bpl) do ( + echo . + echo -------------------- %%f -------------------- + %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:PredicateAbs %%f +) + +for %%f in (quant1.bpl quant2.bpl quant3.bpl quant4.bpl quant5.bpl) do ( + echo . + echo -------------------- %%f -------------------- + %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:HoudiniConst /z3opt:MBQI=true %%f +) diff --git a/Test/AbsHoudini/test1.bpl b/Test/AbsHoudini/test1.bpl index 10015723..80521921 100644 --- a/Test/AbsHoudini/test1.bpl +++ b/Test/AbsHoudini/test1.bpl @@ -1,40 +1,40 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g: bool;
-
-procedure foo()
-modifies g;
-ensures b0() || (!old(g) ==> old(g) == g);
-{
- call AcquireLock();
- call ReleaseLock();
-}
-
-procedure AcquireLock()
-modifies g;
-ensures b1() || old(g) == g;
-{
- g := true;
-}
-
-procedure ReleaseLock()
-modifies g;
-ensures b2() || old(g) == g;
-{
- g := false;
-}
-
-procedure main()
-modifies g;
-{
- g := false;
- call foo();
- assert Assert() || !g;
-}
-
-function {:existential true} b0(): bool;
-function {:existential true} b1(): bool;
-function {:existential true } b2(): bool;
-function {:existential true} Assert(): bool;
-
-// Expected: b0 = false, b1 = true, b2 = true, Assert = false
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var g: bool; + +procedure foo() +modifies g; +ensures b0() || (!old(g) ==> old(g) == g); +{ + call AcquireLock(); + call ReleaseLock(); +} + +procedure AcquireLock() +modifies g; +ensures b1() || old(g) == g; +{ + g := true; +} + +procedure ReleaseLock() +modifies g; +ensures b2() || old(g) == g; +{ + g := false; +} + +procedure main() +modifies g; +{ + g := false; + call foo(); + assert Assert() || !g; +} + +function {:existential true} b0(): bool; +function {:existential true} b1(): bool; +function {:existential true } b2(): bool; +function {:existential true} Assert(): bool; + +// Expected: b0 = false, b1 = true, b2 = true, Assert = false diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl index cb2fe89a..4acc862d 100644 --- a/Test/AbsHoudini/test10.bpl +++ b/Test/AbsHoudini/test10.bpl @@ -1,52 +1,52 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var sdv_7: int;
-var sdv_21: int;
-function {:existential true} b1(): bool;
-function{:existential true} b2(): bool;
-function{:existential true} b3(): bool;
-function{:existential true} b4(): bool;
-
-procedure push(a:int)
-modifies sdv_7, sdv_21;
-{
- sdv_21 := sdv_7;
- sdv_7 := a;
-}
-
-procedure pop()
-modifies sdv_7, sdv_21;
-{
- sdv_7 := sdv_21;
- havoc sdv_21;
-}
-
-procedure foo()
-modifies sdv_7, sdv_21;
-requires {:candidate} b1() || (sdv_7 == 0);
-ensures{:candidate} b2() || (sdv_7 == old(sdv_7));
-{
- call push(2);
- call pop();
- call bar();
-}
-
-procedure bar()
-requires{:candidate} b3() || (sdv_7 == 0);
-ensures{:candidate} b4() || (sdv_7 == old(sdv_7));
-modifies sdv_7, sdv_21;
-{
- call push(1);
- call pop();
-}
-
-procedure main()
-modifies sdv_7, sdv_21;
-{
- sdv_7 := 0;
- call foo();
-}
-
-// Expected: All false
-
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var sdv_7: int; +var sdv_21: int; +function {:existential true} b1(): bool; +function{:existential true} b2(): bool; +function{:existential true} b3(): bool; +function{:existential true} b4(): bool; + +procedure push(a:int) +modifies sdv_7, sdv_21; +{ + sdv_21 := sdv_7; + sdv_7 := a; +} + +procedure pop() +modifies sdv_7, sdv_21; +{ + sdv_7 := sdv_21; + havoc sdv_21; +} + +procedure foo() +modifies sdv_7, sdv_21; +requires {:candidate} b1() || (sdv_7 == 0); +ensures{:candidate} b2() || (sdv_7 == old(sdv_7)); +{ + call push(2); + call pop(); + call bar(); +} + +procedure bar() +requires{:candidate} b3() || (sdv_7 == 0); +ensures{:candidate} b4() || (sdv_7 == old(sdv_7)); +modifies sdv_7, sdv_21; +{ + call push(1); + call pop(); +} + +procedure main() +modifies sdv_7, sdv_21; +{ + sdv_7 := 0; + call foo(); +} + +// Expected: All false + + diff --git a/Test/AbsHoudini/test2.bpl b/Test/AbsHoudini/test2.bpl index 1272e7d9..38ec8c8a 100644 --- a/Test/AbsHoudini/test2.bpl +++ b/Test/AbsHoudini/test2.bpl @@ -1,42 +1,42 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g: int;
-var h: int;
-
-procedure foo()
-modifies g, h;
-ensures b0() || old(g) == g;
-{
- call AcquireLock();
- call ReleaseLock();
-}
-
-procedure AcquireLock()
-modifies g, h;
-ensures b1() || old(g) == g;
-{
- h := g;
- g := 1;
-}
-
-procedure ReleaseLock()
-modifies g, h;
-ensures b2() || old(g) == g;
-{
- g := h;
-}
-
-procedure main()
-modifies g, h;
-{
- g := 0;
- call foo();
- assert Assert() || g == 0;
-}
-
-function {:existential true} b0(): bool;
-function {:existential true} b1(): bool;
-function {:existential true} b2(): bool;
-function {:existential true} Assert(): bool;
-
-// Expected: Assert = false, b0 = false, b1 = true, b2 = true
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var g: int; +var h: int; + +procedure foo() +modifies g, h; +ensures b0() || old(g) == g; +{ + call AcquireLock(); + call ReleaseLock(); +} + +procedure AcquireLock() +modifies g, h; +ensures b1() || old(g) == g; +{ + h := g; + g := 1; +} + +procedure ReleaseLock() +modifies g, h; +ensures b2() || old(g) == g; +{ + g := h; +} + +procedure main() +modifies g, h; +{ + g := 0; + call foo(); + assert Assert() || g == 0; +} + +function {:existential true} b0(): bool; +function {:existential true} b1(): bool; +function {:existential true} b2(): bool; +function {:existential true} Assert(): bool; + +// Expected: Assert = false, b0 = false, b1 = true, b2 = true diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl index 118a1c99..65f311f6 100644 --- a/Test/AbsHoudini/test7.bpl +++ b/Test/AbsHoudini/test7.bpl @@ -1,21 +1,21 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} Assert() : bool;
-
-var g: int;
-
-procedure main()
-modifies g;
-{
- g := 0;
- call foo();
- assert Assert() || g == 1;
-}
-
-procedure foo()
-modifies g;
-{
- g := g + 1;
-}
-
-// Expected: Assert = false
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} Assert() : bool; + +var g: int; + +procedure main() +modifies g; +{ + g := 0; + call foo(); + assert Assert() || g == 1; +} + +procedure foo() +modifies g; +{ + g := g + 1; +} + +// Expected: Assert = false diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl index f9a9afaa..1a79d188 100644 --- a/Test/AbsHoudini/test8.bpl +++ b/Test/AbsHoudini/test8.bpl @@ -1,27 +1,27 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:existential true} Assert(): bool;
-
-var g: int;
-
-procedure main()
-modifies g;
-{
- g := 0;
- call foo();
- assert Assert() || g == 1;
-}
-
-procedure {:inline 1} foo()
-modifies g;
-{
- call bar();
-}
-
-procedure bar()
-modifies g;
-{
- g := g + 1;
-}
-
-// Expected: Assert = false
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:existential true} Assert(): bool; + +var g: int; + +procedure main() +modifies g; +{ + g := 0; + call foo(); + assert Assert() || g == 1; +} + +procedure {:inline 1} foo() +modifies g; +{ + call bar(); +} + +procedure bar() +modifies g; +{ + g := g + 1; +} + +// Expected: Assert = false diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl index 7d624167..9e7778eb 100644 --- a/Test/AbsHoudini/test9.bpl +++ b/Test/AbsHoudini/test9.bpl @@ -1,92 +1,92 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var v1: int;
-var v2: int;
-var v3: int;
-function{:existential true} b1(): bool;
-function{:existential true} b2(): bool;
-function{:existential true} b3(): bool;
-function{:existential true} b4(): bool;
-function{:existential true} b5(): bool;
-function{:existential true} b6(): bool;
-function{:existential true} b7(): bool;
-function{:existential true} b8(): bool;
-function{:existential true} b9(): bool;
-function{:existential true} b10(): bool;
-function{:existential true} b11(): bool;
-function{:existential true} b12(): bool;
-function{:existential true} b13(): bool;
-function{:existential true} b14(): bool;
-function{:existential true} b15(): bool;
-function{:existential true} b16(): bool;
-
-procedure push()
-requires {:candidate} b1() || v1 == 0;
-requires {:candidate} b2() || v1 == 1;
-ensures {:candidate} b3() || v1 == 0;
-ensures {:candidate} b4() || v1 == 1;
-modifies v1,v2;
-{
- v2 := v1;
- v1 := 1;
-}
-
-procedure pop()
-modifies v1,v2;
-requires {:candidate} b5() || v1 == 0;
-requires {:candidate} b6() || v1 == 1;
-ensures {:candidate} b7() || v1 == 0;
-ensures {:candidate} b8() || v1 == 1;
-{
- v1 := v2;
- havoc v2;
-}
-
-procedure foo()
-modifies v1,v2;
-requires {:candidate} b9() || v1 == 0;
-requires {:candidate} b10() || v1 == 1;
-ensures {:candidate} b11() || v1 == 0;
-ensures {:candidate} b12() || v1 == 1;
-{
- call push();
- call pop();
-}
-
-procedure bar()
-modifies v1,v2;
-requires {:candidate} b13() || v1 == 0;
-requires {:candidate} b14() || v1 == 1;
-ensures {:candidate} b15() || v1 == 0;
-ensures {:candidate} b16() || v1 == 1;
-{
- call push();
- call pop();
-}
-
-procedure main()
-modifies v1,v2;
-{
- v1 := 1;
- call foo();
- havoc v1;
- call bar();
-}
-
-// Expected:
-//b1 = true
-//b2 = true
-//b3 = true
-//b4 = false
-//b5 = true
-//b6 = false
-//b7 = true
-//b8 = true
-//b9 = true
-//b10 = false
-//b11 = true
-//b12 = false
-//b13 = true
-//b14 = true
-//b15 = true
-//b16 = true
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var v1: int; +var v2: int; +var v3: int; +function{:existential true} b1(): bool; +function{:existential true} b2(): bool; +function{:existential true} b3(): bool; +function{:existential true} b4(): bool; +function{:existential true} b5(): bool; +function{:existential true} b6(): bool; +function{:existential true} b7(): bool; +function{:existential true} b8(): bool; +function{:existential true} b9(): bool; +function{:existential true} b10(): bool; +function{:existential true} b11(): bool; +function{:existential true} b12(): bool; +function{:existential true} b13(): bool; +function{:existential true} b14(): bool; +function{:existential true} b15(): bool; +function{:existential true} b16(): bool; + +procedure push() +requires {:candidate} b1() || v1 == 0; +requires {:candidate} b2() || v1 == 1; +ensures {:candidate} b3() || v1 == 0; +ensures {:candidate} b4() || v1 == 1; +modifies v1,v2; +{ + v2 := v1; + v1 := 1; +} + +procedure pop() +modifies v1,v2; +requires {:candidate} b5() || v1 == 0; +requires {:candidate} b6() || v1 == 1; +ensures {:candidate} b7() || v1 == 0; +ensures {:candidate} b8() || v1 == 1; +{ + v1 := v2; + havoc v2; +} + +procedure foo() +modifies v1,v2; +requires {:candidate} b9() || v1 == 0; +requires {:candidate} b10() || v1 == 1; +ensures {:candidate} b11() || v1 == 0; +ensures {:candidate} b12() || v1 == 1; +{ + call push(); + call pop(); +} + +procedure bar() +modifies v1,v2; +requires {:candidate} b13() || v1 == 0; +requires {:candidate} b14() || v1 == 1; +ensures {:candidate} b15() || v1 == 0; +ensures {:candidate} b16() || v1 == 1; +{ + call push(); + call pop(); +} + +procedure main() +modifies v1,v2; +{ + v1 := 1; + call foo(); + havoc v1; + call bar(); +} + +// Expected: +//b1 = true +//b2 = true +//b3 = true +//b4 = false +//b5 = true +//b6 = false +//b7 = true +//b8 = true +//b9 = true +//b10 = false +//b11 = true +//b12 = false +//b13 = true +//b14 = true +//b15 = true +//b16 = true |