From 75416c24e78d9992c10fbb86ba458e813acf943d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 27 May 2014 19:55:30 +0100 Subject: Convert the AbsHoudini tests to lit tests. They weren't being run by the old infrastructure so I have not bothered to update the Answer file. These tests are still disabled by the lit.local.cfg file in the AbsHoudini folder because the following tests fail or weren't even being run previously (these are left unresolved because I do not know how these tests are meant to be run) UNRESOLVED: Boogie :: AbsHoudini/f1.bpl (1 of 32) UNRESOLVED: Boogie :: AbsHoudini/imp1.bpl (7 of 32) UNRESOLVED: Boogie :: AbsHoudini/int1.bpl (8 of 32) UNRESOLVED: Boogie :: AbsHoudini/multi.bpl (9 of 32) FAIL: Boogie :: AbsHoudini/quant3.bpl (22 of 32) FAIL: Boogie :: AbsHoudini/quant5.bpl (28 of 32) --- Test/AbsHoudini/fail1.bpl | 2 ++ Test/AbsHoudini/fail1.bpl.expect | 11 +++++++ Test/AbsHoudini/houd1.bpl | 2 ++ Test/AbsHoudini/houd1.bpl.expect | 6 ++++ Test/AbsHoudini/houd10.bpl | 2 ++ Test/AbsHoudini/houd10.bpl.expect | 18 +++++++++++ Test/AbsHoudini/houd11.bpl | 2 ++ Test/AbsHoudini/houd11.bpl.expect | 6 ++++ Test/AbsHoudini/houd12.bpl | 2 ++ Test/AbsHoudini/houd12.bpl.expect | 34 ++++++++++++++++++++ Test/AbsHoudini/houd2.bpl | 2 ++ Test/AbsHoudini/houd2.bpl.expect | 14 +++++++++ Test/AbsHoudini/houd3.bpl | 2 ++ Test/AbsHoudini/houd3.bpl.expect | 14 +++++++++ Test/AbsHoudini/houd4.bpl | 2 ++ Test/AbsHoudini/houd4.bpl.expect | 22 +++++++++++++ Test/AbsHoudini/houd5.bpl | 2 ++ Test/AbsHoudini/houd5.bpl.expect | 26 +++++++++++++++ Test/AbsHoudini/houd6.bpl | 2 ++ Test/AbsHoudini/houd6.bpl.expect | 38 ++++++++++++++++++++++ Test/AbsHoudini/houd7.bpl | 2 ++ Test/AbsHoudini/houd7.bpl.expect | 18 +++++++++++ Test/AbsHoudini/houd8.bpl | 2 ++ Test/AbsHoudini/houd8.bpl.expect | 14 +++++++++ Test/AbsHoudini/pred1.bpl | 2 ++ Test/AbsHoudini/pred1.bpl.expect | 14 +++++++++ Test/AbsHoudini/pred2.bpl | 2 ++ Test/AbsHoudini/pred2.bpl.expect | 6 ++++ Test/AbsHoudini/pred3.bpl | 2 ++ Test/AbsHoudini/pred3.bpl.expect | 14 +++++++++ Test/AbsHoudini/pred4.bpl | 2 ++ Test/AbsHoudini/pred4.bpl.expect | 10 ++++++ Test/AbsHoudini/pred5.bpl | 2 ++ Test/AbsHoudini/pred5.bpl.expect | 6 ++++ Test/AbsHoudini/quant1.bpl | 2 ++ Test/AbsHoudini/quant1.bpl.expect | 6 ++++ Test/AbsHoudini/quant2.bpl | 2 ++ Test/AbsHoudini/quant2.bpl.expect | 6 ++++ Test/AbsHoudini/quant3.bpl | 2 ++ Test/AbsHoudini/quant3.bpl.expect | 6 ++++ Test/AbsHoudini/quant4.bpl | 2 ++ Test/AbsHoudini/quant4.bpl.expect | 6 ++++ Test/AbsHoudini/quant5.bpl | 2 ++ Test/AbsHoudini/quant5.bpl.expect | 6 ++++ Test/AbsHoudini/test1.bpl | 2 ++ Test/AbsHoudini/test1.bpl.expect | 18 +++++++++++ Test/AbsHoudini/test10.bpl | 2 ++ Test/AbsHoudini/test10.bpl.expect | 18 +++++++++++ Test/AbsHoudini/test2.bpl | 2 ++ Test/AbsHoudini/test2.bpl.expect | 18 +++++++++++ Test/AbsHoudini/test7.bpl | 2 ++ Test/AbsHoudini/test7.bpl.expect | 6 ++++ Test/AbsHoudini/test8.bpl | 2 ++ Test/AbsHoudini/test8.bpl.expect | 6 ++++ Test/AbsHoudini/test9.bpl | 2 ++ Test/AbsHoudini/test9.bpl.expect | 66 +++++++++++++++++++++++++++++++++++++++ 56 files changed, 489 insertions(+) create mode 100644 Test/AbsHoudini/fail1.bpl.expect create mode 100644 Test/AbsHoudini/houd1.bpl.expect create mode 100644 Test/AbsHoudini/houd10.bpl.expect create mode 100644 Test/AbsHoudini/houd11.bpl.expect create mode 100644 Test/AbsHoudini/houd12.bpl.expect create mode 100644 Test/AbsHoudini/houd2.bpl.expect create mode 100644 Test/AbsHoudini/houd3.bpl.expect create mode 100644 Test/AbsHoudini/houd4.bpl.expect create mode 100644 Test/AbsHoudini/houd5.bpl.expect create mode 100644 Test/AbsHoudini/houd6.bpl.expect create mode 100644 Test/AbsHoudini/houd7.bpl.expect create mode 100644 Test/AbsHoudini/houd8.bpl.expect create mode 100644 Test/AbsHoudini/pred1.bpl.expect create mode 100644 Test/AbsHoudini/pred2.bpl.expect create mode 100644 Test/AbsHoudini/pred3.bpl.expect create mode 100644 Test/AbsHoudini/pred4.bpl.expect create mode 100644 Test/AbsHoudini/pred5.bpl.expect create mode 100644 Test/AbsHoudini/quant1.bpl.expect create mode 100644 Test/AbsHoudini/quant2.bpl.expect create mode 100644 Test/AbsHoudini/quant3.bpl.expect create mode 100644 Test/AbsHoudini/quant4.bpl.expect create mode 100644 Test/AbsHoudini/quant5.bpl.expect create mode 100644 Test/AbsHoudini/test1.bpl.expect create mode 100644 Test/AbsHoudini/test10.bpl.expect create mode 100644 Test/AbsHoudini/test2.bpl.expect create mode 100644 Test/AbsHoudini/test7.bpl.expect create mode 100644 Test/AbsHoudini/test8.bpl.expect create mode 100644 Test/AbsHoudini/test9.bpl.expect (limited to 'Test/AbsHoudini') 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 -- cgit v1.2.3