diff options
Diffstat (limited to 'Test')
59 files changed, 597 insertions, 4 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 diff --git a/Test/README.md b/Test/README.md index 98013581..4446aa4f 100644 --- a/Test/README.md +++ b/Test/README.md @@ -110,8 +110,9 @@ The RUN lines may use several substitutions - ``%boogie`` expands to the absolute path to the Boogie executable with any set
options and prefixed by ``mono`` on non Windows platforms
-- ``%diff`` expands to the diff tool being used. This is ``diff`` on non Windows
- platforms and ``fc`` on Windows.
+- ``%diff`` expands to the diff tool being used. This is ``diff`` on non
+ Windows platforms and ``pydiff`` on Windows. Do not use the ``fc`` tool
+ because it is buggy when tests are run concurrently.
- ``%OutputCheck`` expands to the absolute path to the OutputCheck tool
diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index 9cd85ef6..e103edde 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -111,13 +111,16 @@ else: lit_config.warning('Skipping solver sanity check on Windows') # Add diff tool substitution +commonDiffFlags=' --unified=3 --strip-trailing-cr --ignore-all-space' diffExecutable = None if os.name == 'posix': - diffExecutable = 'diff --unified=3 --strip-trailing-cr --ignore-all-space' + diffExecutable = 'diff' + commonDiffFlags elif os.name == 'nt': - diffExecutable = 'fc /W' + pydiff = os.path.join(config.test_source_root, 'pydiff.py') + diffExecutable = sys.executable + ' ' + pydiff + commonDiffFlags else: lit_config.fatal('Unsupported platform') +lit_config.note("Using diff tool '{}'".format(diffExecutable)) config.substitutions.append( ('%diff', diffExecutable )) diff --git a/Test/pydiff.py b/Test/pydiff.py new file mode 100644 index 00000000..407fe251 --- /dev/null +++ b/Test/pydiff.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python +""" +Simple driver around python's difflib that implements a basic ``diff`` like +tool. This exists to provide a simple ``diff`` like tool that will run on +Windows where only the ``fc`` tool is available. +""" +import argparse +import difflib +import os +import sys + + +def main(args): + parser = argparse.ArgumentParser(formatter_class=argparse.RawDescriptionHelpFormatter, + description=__doc__ + ) + # Open in binary mode so python doesn't try and do + # universal line endings for us. + parser.add_argument('from-file', + type=argparse.FileType('rb'), + ) + parser.add_argument('to-file', + type=argparse.FileType('rb'), + ) + parser.add_argument('-U','--unified=', + type=int, + default=3, + help='Number of context lines to show. ' + 'Default %(default)s' + ) + parser.add_argument('--strip-trailing-cr', + action='store_true', + help='strip trailing carriage return when comparing' + ) + parser.add_argument('--ignore-all-space','-w', + action='store_true', + help='Ignore all whitespace characters when comparing' + ) + + parsedArgs = parser.parse_args(args) + fromFile, fromFileName = preProcess(getattr(parsedArgs,'from-file'), + parsedArgs.strip_trailing_cr, + parsedArgs.ignore_all_space + ) + toFile, toFileName = preProcess(getattr(parsedArgs,'to-file'), + parsedArgs.strip_trailing_cr, + parsedArgs.ignore_all_space + ) + + result = difflib.unified_diff(fromFile, + toFile, + fromFileName, + toFileName, + n=getattr(parsedArgs,'unified='), + ) + # Force lazy computation to happen now + result = list(result) + + if len(result) == 0: + # Files are identical + return 0 + else: + for l in result: + sys.stdout.write(l) + return 1 + +def preProcess(openFile, stripTrailingCR=False, ignoreAllSpace=False): + """ + Helper function to read lines in a file and do any necessary + pre-processing + """ + original = openFile.readlines() + + # Translation table deletes white space characters Note we don't remove + # newline characters because this will create a mess when outputting the + # diff. Is this the right behaviour? + deleteChars=' \t' + translationTable = str.maketrans('','', deleteChars) + + copy = [ ] + for line in original: + newLine = str(line.decode()) + + if stripTrailingCR: + if newLine[-2:] == '\r\n' or newLine[-2:] == '\n\r': + newLine = newLine[:-2] + '\n' + + if ignoreAllSpace: + newLine = newLine.translate(translationTable) + + copy.append(newLine) + + return (copy, openFile.name) + +def getFileName(openFile): + return openFile.name + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) + |