diff options
56 files changed, 489 insertions, 0 deletions
diff --git a/Test/AbsHoudini/fail1.bpl b/Test/AbsHoudini/fail1.bpl index abbd015b..5e15340c 100644 --- a/Test/AbsHoudini/fail1.bpl +++ b/Test/AbsHoudini/fail1.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/fail1.bpl.expect b/Test/AbsHoudini/fail1.bpl.expect new file mode 100644 index 00000000..e987f773 --- /dev/null +++ b/Test/AbsHoudini/fail1.bpl.expect @@ -0,0 +1,11 @@ +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 diff --git a/Test/AbsHoudini/houd1.bpl b/Test/AbsHoudini/houd1.bpl index fc3d5713..0a8ebeb3 100644 --- a/Test/AbsHoudini/houd1.bpl +++ b/Test/AbsHoudini/houd1.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/houd1.bpl.expect b/Test/AbsHoudini/houd1.bpl.expect new file mode 100644 index 00000000..0b023466 --- /dev/null +++ b/Test/AbsHoudini/houd1.bpl.expect @@ -0,0 +1,6 @@ +function {:existential true} {:inline} b1(x: bool) : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl index bb0c65e7..6ee73b9a 100644 --- a/Test/AbsHoudini/houd10.bpl +++ b/Test/AbsHoudini/houd10.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/houd10.bpl.expect b/Test/AbsHoudini/houd10.bpl.expect new file mode 100644 index 00000000..d427a9f2 --- /dev/null +++ b/Test/AbsHoudini/houd10.bpl.expect @@ -0,0 +1,18 @@ +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 diff --git a/Test/AbsHoudini/houd11.bpl b/Test/AbsHoudini/houd11.bpl index 78087744..dbde4f37 100644 --- a/Test/AbsHoudini/houd11.bpl +++ b/Test/AbsHoudini/houd11.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
+// RUN: %diff %s.expect %t
function {:existential true} Assert() : bool;
var fooVar: int;
diff --git a/Test/AbsHoudini/houd11.bpl.expect b/Test/AbsHoudini/houd11.bpl.expect new file mode 100644 index 00000000..13aff08c --- /dev/null +++ b/Test/AbsHoudini/houd11.bpl.expect @@ -0,0 +1,6 @@ +function {:existential true} {:inline} Assert() : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/houd12.bpl b/Test/AbsHoudini/houd12.bpl index b3a1a6db..ac46ef62 100644 --- a/Test/AbsHoudini/houd12.bpl +++ b/Test/AbsHoudini/houd12.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/houd12.bpl.expect b/Test/AbsHoudini/houd12.bpl.expect new file mode 100644 index 00000000..aefaac93 --- /dev/null +++ b/Test/AbsHoudini/houd12.bpl.expect @@ -0,0 +1,34 @@ +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 diff --git a/Test/AbsHoudini/houd2.bpl b/Test/AbsHoudini/houd2.bpl index fd2611e2..c4d8e4e0 100644 --- a/Test/AbsHoudini/houd2.bpl +++ b/Test/AbsHoudini/houd2.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/houd2.bpl.expect b/Test/AbsHoudini/houd2.bpl.expect new file mode 100644 index 00000000..6fe401ad --- /dev/null +++ b/Test/AbsHoudini/houd2.bpl.expect @@ -0,0 +1,14 @@ +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 diff --git a/Test/AbsHoudini/houd3.bpl b/Test/AbsHoudini/houd3.bpl index 81f11018..a37b5874 100644 --- a/Test/AbsHoudini/houd3.bpl +++ b/Test/AbsHoudini/houd3.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/houd3.bpl.expect b/Test/AbsHoudini/houd3.bpl.expect new file mode 100644 index 00000000..780edc91 --- /dev/null +++ b/Test/AbsHoudini/houd3.bpl.expect @@ -0,0 +1,14 @@ +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 diff --git a/Test/AbsHoudini/houd4.bpl b/Test/AbsHoudini/houd4.bpl index 01ee6707..2fc339d9 100644 --- a/Test/AbsHoudini/houd4.bpl +++ b/Test/AbsHoudini/houd4.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/houd4.bpl.expect b/Test/AbsHoudini/houd4.bpl.expect new file mode 100644 index 00000000..a6756239 --- /dev/null +++ b/Test/AbsHoudini/houd4.bpl.expect @@ -0,0 +1,22 @@ +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 diff --git a/Test/AbsHoudini/houd5.bpl b/Test/AbsHoudini/houd5.bpl index afbaa81c..8a08b5cf 100644 --- a/Test/AbsHoudini/houd5.bpl +++ b/Test/AbsHoudini/houd5.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/houd5.bpl.expect b/Test/AbsHoudini/houd5.bpl.expect new file mode 100644 index 00000000..12144524 --- /dev/null +++ b/Test/AbsHoudini/houd5.bpl.expect @@ -0,0 +1,26 @@ +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 diff --git a/Test/AbsHoudini/houd6.bpl b/Test/AbsHoudini/houd6.bpl index e4927901..209e2f01 100644 --- a/Test/AbsHoudini/houd6.bpl +++ b/Test/AbsHoudini/houd6.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/houd6.bpl.expect b/Test/AbsHoudini/houd6.bpl.expect new file mode 100644 index 00000000..f5c02d70 --- /dev/null +++ b/Test/AbsHoudini/houd6.bpl.expect @@ -0,0 +1,38 @@ +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 diff --git a/Test/AbsHoudini/houd7.bpl b/Test/AbsHoudini/houd7.bpl index ef3293db..6df7b428 100644 --- a/Test/AbsHoudini/houd7.bpl +++ b/Test/AbsHoudini/houd7.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/houd7.bpl.expect b/Test/AbsHoudini/houd7.bpl.expect new file mode 100644 index 00000000..ce1675e4 --- /dev/null +++ b/Test/AbsHoudini/houd7.bpl.expect @@ -0,0 +1,18 @@ +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 diff --git a/Test/AbsHoudini/houd8.bpl b/Test/AbsHoudini/houd8.bpl index 8be7f3db..e5b88466 100644 --- a/Test/AbsHoudini/houd8.bpl +++ b/Test/AbsHoudini/houd8.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/houd8.bpl.expect b/Test/AbsHoudini/houd8.bpl.expect new file mode 100644 index 00000000..605ec988 --- /dev/null +++ b/Test/AbsHoudini/houd8.bpl.expect @@ -0,0 +1,14 @@ +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 diff --git a/Test/AbsHoudini/pred1.bpl b/Test/AbsHoudini/pred1.bpl index fc37a15b..0c2d7f10 100644 --- a/Test/AbsHoudini/pred1.bpl +++ b/Test/AbsHoudini/pred1.bpl @@ -1,3 +1,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;
diff --git a/Test/AbsHoudini/pred1.bpl.expect b/Test/AbsHoudini/pred1.bpl.expect new file mode 100644 index 00000000..0e3d3333 --- /dev/null +++ b/Test/AbsHoudini/pred1.bpl.expect @@ -0,0 +1,14 @@ +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 diff --git a/Test/AbsHoudini/pred2.bpl b/Test/AbsHoudini/pred2.bpl index 3ce948ce..9e93495f 100644 --- a/Test/AbsHoudini/pred2.bpl +++ b/Test/AbsHoudini/pred2.bpl @@ -1,3 +1,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;
diff --git a/Test/AbsHoudini/pred2.bpl.expect b/Test/AbsHoudini/pred2.bpl.expect new file mode 100644 index 00000000..55e46035 --- /dev/null +++ b/Test/AbsHoudini/pred2.bpl.expect @@ -0,0 +1,6 @@ +function {:existential true} {:inline} b0(x: bool) : bool +{ + x +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/pred3.bpl b/Test/AbsHoudini/pred3.bpl index 450efde4..1cb36798 100644 --- a/Test/AbsHoudini/pred3.bpl +++ b/Test/AbsHoudini/pred3.bpl @@ -1,3 +1,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;
diff --git a/Test/AbsHoudini/pred3.bpl.expect b/Test/AbsHoudini/pred3.bpl.expect new file mode 100644 index 00000000..0e3d3333 --- /dev/null +++ b/Test/AbsHoudini/pred3.bpl.expect @@ -0,0 +1,14 @@ +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 diff --git a/Test/AbsHoudini/pred4.bpl b/Test/AbsHoudini/pred4.bpl index d4741720..9c814e3b 100644 --- a/Test/AbsHoudini/pred4.bpl +++ b/Test/AbsHoudini/pred4.bpl @@ -1,3 +1,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;
diff --git a/Test/AbsHoudini/pred4.bpl.expect b/Test/AbsHoudini/pred4.bpl.expect new file mode 100644 index 00000000..ec1d9517 --- /dev/null +++ b/Test/AbsHoudini/pred4.bpl.expect @@ -0,0 +1,10 @@ +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 diff --git a/Test/AbsHoudini/pred5.bpl b/Test/AbsHoudini/pred5.bpl index 6940e820..762a354f 100644 --- a/Test/AbsHoudini/pred5.bpl +++ b/Test/AbsHoudini/pred5.bpl @@ -1,3 +1,5 @@ +// 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()
diff --git a/Test/AbsHoudini/pred5.bpl.expect b/Test/AbsHoudini/pred5.bpl.expect new file mode 100644 index 00000000..a5e1c73d --- /dev/null +++ b/Test/AbsHoudini/pred5.bpl.expect @@ -0,0 +1,6 @@ +function {:existential true} {:inline} b1(x: bool) : bool +{ + x +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/quant1.bpl b/Test/AbsHoudini/quant1.bpl index e12525b6..a5709736 100644 --- a/Test/AbsHoudini/quant1.bpl +++ b/Test/AbsHoudini/quant1.bpl @@ -1,3 +1,5 @@ +// 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 ()
diff --git a/Test/AbsHoudini/quant1.bpl.expect b/Test/AbsHoudini/quant1.bpl.expect new file mode 100644 index 00000000..7d06cb21 --- /dev/null +++ b/Test/AbsHoudini/quant1.bpl.expect @@ -0,0 +1,6 @@ +function {:existential true} {:absdomain "IA[Intervals]"} {:inline} b1(x: int) : bool +{ + x >= 0 && x <= 2 +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/quant2.bpl b/Test/AbsHoudini/quant2.bpl index 5a491877..2f291fca 100644 --- a/Test/AbsHoudini/quant2.bpl +++ b/Test/AbsHoudini/quant2.bpl @@ -1,3 +1,5 @@ +// 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()
diff --git a/Test/AbsHoudini/quant2.bpl.expect b/Test/AbsHoudini/quant2.bpl.expect new file mode 100644 index 00000000..0610db26 --- /dev/null +++ b/Test/AbsHoudini/quant2.bpl.expect @@ -0,0 +1,6 @@ +function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool +{ + x >= 0 && x <= 1 +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/quant3.bpl b/Test/AbsHoudini/quant3.bpl index cc0ef79e..10fb72c7 100644 --- a/Test/AbsHoudini/quant3.bpl +++ b/Test/AbsHoudini/quant3.bpl @@ -1,3 +1,5 @@ +// 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 ()
diff --git a/Test/AbsHoudini/quant3.bpl.expect b/Test/AbsHoudini/quant3.bpl.expect new file mode 100644 index 00000000..d43073ab --- /dev/null +++ b/Test/AbsHoudini/quant3.bpl.expect @@ -0,0 +1,6 @@ +function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool +{ + x >= 0 && x <= 0 +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/quant4.bpl b/Test/AbsHoudini/quant4.bpl index 55947f1f..99c37572 100644 --- a/Test/AbsHoudini/quant4.bpl +++ b/Test/AbsHoudini/quant4.bpl @@ -1,3 +1,5 @@ +// 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 ()
diff --git a/Test/AbsHoudini/quant4.bpl.expect b/Test/AbsHoudini/quant4.bpl.expect new file mode 100644 index 00000000..07f98295 --- /dev/null +++ b/Test/AbsHoudini/quant4.bpl.expect @@ -0,0 +1,6 @@ +function {:existential true} {:absdomain "IA[HoudiniConst]"} {:inline} b1() : bool +{ + true +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/quant5.bpl b/Test/AbsHoudini/quant5.bpl index dfc44e47..83e6e68a 100644 --- a/Test/AbsHoudini/quant5.bpl +++ b/Test/AbsHoudini/quant5.bpl @@ -1,3 +1,5 @@ +// 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 ()
diff --git a/Test/AbsHoudini/quant5.bpl.expect b/Test/AbsHoudini/quant5.bpl.expect new file mode 100644 index 00000000..b74f5abc --- /dev/null +++ b/Test/AbsHoudini/quant5.bpl.expect @@ -0,0 +1,6 @@ +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/test1.bpl b/Test/AbsHoudini/test1.bpl index 5884cf7b..ba18cf15 100644 --- a/Test/AbsHoudini/test1.bpl +++ b/Test/AbsHoudini/test1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t
+// RUN: %diff %s.expect %t
var g: bool;
procedure foo()
diff --git a/Test/AbsHoudini/test1.bpl.expect b/Test/AbsHoudini/test1.bpl.expect new file mode 100644 index 00000000..ecc2a8fd --- /dev/null +++ b/Test/AbsHoudini/test1.bpl.expect @@ -0,0 +1,18 @@ +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 diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl index a30c3159..76a02e23 100644 --- a/Test/AbsHoudini/test10.bpl +++ b/Test/AbsHoudini/test10.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/test10.bpl.expect b/Test/AbsHoudini/test10.bpl.expect new file mode 100644 index 00000000..c9e99b13 --- /dev/null +++ b/Test/AbsHoudini/test10.bpl.expect @@ -0,0 +1,18 @@ +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 diff --git a/Test/AbsHoudini/test2.bpl b/Test/AbsHoudini/test2.bpl index bfd78363..8c1717bf 100644 --- a/Test/AbsHoudini/test2.bpl +++ b/Test/AbsHoudini/test2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t
+// RUN: %diff %s.expect %t
var g: int;
var h: int;
diff --git a/Test/AbsHoudini/test2.bpl.expect b/Test/AbsHoudini/test2.bpl.expect new file mode 100644 index 00000000..ecc2a8fd --- /dev/null +++ b/Test/AbsHoudini/test2.bpl.expect @@ -0,0 +1,18 @@ +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 diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl index bfe8a32d..d9500308 100644 --- a/Test/AbsHoudini/test7.bpl +++ b/Test/AbsHoudini/test7.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/test7.bpl.expect b/Test/AbsHoudini/test7.bpl.expect new file mode 100644 index 00000000..82afc94e --- /dev/null +++ b/Test/AbsHoudini/test7.bpl.expect @@ -0,0 +1,6 @@ +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl index 6c55016a..0b00bc19 100644 --- a/Test/AbsHoudini/test8.bpl +++ b/Test/AbsHoudini/test8.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/test8.bpl.expect b/Test/AbsHoudini/test8.bpl.expect new file mode 100644 index 00000000..82afc94e --- /dev/null +++ b/Test/AbsHoudini/test8.bpl.expect @@ -0,0 +1,6 @@ +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl index c08edf6b..221234e5 100644 --- a/Test/AbsHoudini/test9.bpl +++ b/Test/AbsHoudini/test9.bpl @@ -1,3 +1,5 @@ +// 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;
diff --git a/Test/AbsHoudini/test9.bpl.expect b/Test/AbsHoudini/test9.bpl.expect new file mode 100644 index 00000000..ae5e9286 --- /dev/null +++ b/Test/AbsHoudini/test9.bpl.expect @@ -0,0 +1,66 @@ +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 |