diff options
Diffstat (limited to 'Test/optimization')
-rw-r--r-- | Test/optimization/Optimization0.bpl | 84 | ||||
-rw-r--r-- | Test/optimization/Optimization0.bpl.expect | 135 | ||||
-rw-r--r-- | Test/optimization/Optimization1.bpl | 32 | ||||
-rw-r--r-- | Test/optimization/Optimization1.bpl.expect | 5 | ||||
-rw-r--r-- | Test/optimization/Optimization2.bpl | 12 | ||||
-rw-r--r-- | Test/optimization/Optimization2.bpl.expect | 3 | ||||
-rw-r--r-- | Test/optimization/Optimization3.bpl | 20 | ||||
-rw-r--r-- | Test/optimization/Optimization3.bpl.expect | 31 | ||||
-rw-r--r-- | Test/optimization/lit.local.cfg | 3 |
9 files changed, 325 insertions, 0 deletions
diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl new file mode 100644 index 00000000..24424e53 --- /dev/null +++ b/Test/optimization/Optimization0.bpl @@ -0,0 +1,84 @@ +// RUN: %boogie /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function may_fail(f: int) : bool; + +procedure test0() +{ + var x: int; + + havoc x; + assume 42 < x; + assume {:minimize x} true; + assert may_fail(x); +} + +procedure test1() +{ + var x: int; + + x := 24; + if (*) { + x := 42; + } + assume {:minimize x} true; + assert may_fail(x); +} + +procedure test2() +{ + var x: int; + + x := 1; + while (*) { + x := x + 1; + } + assume {:minimize x} true; + assert x < 10; +} + +procedure test3() +{ + var x: int; + + havoc x; + assume x < 42; + assume {:maximize x} true; + assert may_fail(x); +} + +procedure test4() +{ + var x: int; + + x := 24; + if (*) { + x := 42; + } + assume {:maximize x} true; + assert may_fail(x); +} + +procedure test5() +{ + var x: int; + + x := 1; + while (*) { + x := x - 1; + } + assume {:maximize x} true; + assert x < 1; +} + +procedure test6() +{ + var x: int; + + x := 1; + if (*) { + x := 2; + } + assume {:maximize x} true; + assert may_fail(x); +} diff --git a/Test/optimization/Optimization0.bpl.expect b/Test/optimization/Optimization0.bpl.expect new file mode 100644 index 00000000..f5a51848 --- /dev/null +++ b/Test/optimization/Optimization0.bpl.expect @@ -0,0 +1,135 @@ +*** MODEL +%lbl%@280 -> false +%lbl%+260 -> true +%lbl%+39 -> true +x@0 -> 43 +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 43 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(13,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(10,5): anon0 +*** MODEL +%lbl%@321 -> false +%lbl%+299 -> true +%lbl%+66 -> true +%lbl%+68 -> true +x@0@@0 -> 24 +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 24 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(25,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(20,7): anon0 + Optimization0.bpl(21,5): anon3_Else + Optimization0.bpl(24,5): anon2 +*** MODEL +%lbl%@353 -> false +%lbl%+335 -> true +%lbl%+95 -> true +%lbl%+99 -> true +x@0@@1 -> 10 +tickleBool -> { + true -> true + false -> true + else -> true +} +*** END_MODEL +Optimization0.bpl(37,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(32,7): anon0 + Optimization0.bpl(33,5): anon3_LoopHead + Optimization0.bpl(33,5): anon3_LoopDone +*** MODEL +%lbl%@386 -> false +%lbl%+122 -> true +%lbl%+375 -> true +x@0@@2 -> 41 +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 41 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(47,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(44,5): anon0 +*** MODEL +%lbl%@414 -> false +%lbl%+147 -> true +%lbl%+151 -> true +%lbl%+392 -> true +x@0@@3 -> 42 +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 42 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(59,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(54,7): anon0 + Optimization0.bpl(56,11): anon3_Then + Optimization0.bpl(58,5): anon2 +*** MODEL +%lbl%@446 -> false +%lbl%+178 -> true +%lbl%+182 -> true +%lbl%+428 -> true +x@0@@4 -> 1 +tickleBool -> { + true -> true + false -> true + else -> true +} +*** END_MODEL +Optimization0.bpl(71,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(66,7): anon0 + Optimization0.bpl(67,5): anon3_LoopHead + Optimization0.bpl(67,5): anon3_LoopDone +*** MODEL +%lbl%@490 -> false +%lbl%+209 -> true +%lbl%+213 -> true +%lbl%+468 -> true +x@0@@5 -> 2 +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 2 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(83,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(78,7): anon0 + Optimization0.bpl(80,11): anon3_Then + Optimization0.bpl(82,5): anon2 + +Boogie program verifier finished with 0 verified, 7 errors diff --git a/Test/optimization/Optimization1.bpl b/Test/optimization/Optimization1.bpl new file mode 100644 index 00000000..60df1edd --- /dev/null +++ b/Test/optimization/Optimization1.bpl @@ -0,0 +1,32 @@ +// RUN: %boogie /noVerify /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:minimize} true; +} + +procedure test1(n: int) +{ + assume {:maximize} true; +} + +procedure test2(n: int) +{ + assume {:minimize n, n} true; +} + +procedure test3(n: int) +{ + assume {:maximize n, n} true; +} + +procedure test4(n: int) +{ + assume {:minimize true} true; +} + +procedure test5(n: int) +{ + assume {:maximize true} true; +} diff --git a/Test/optimization/Optimization1.bpl.expect b/Test/optimization/Optimization1.bpl.expect new file mode 100644 index 00000000..d8508807 --- /dev/null +++ b/Test/optimization/Optimization1.bpl.expect @@ -0,0 +1,5 @@ +Optimization1.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument +Optimization1.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument +Optimization1.bpl(16,11): Error: attributes :minimize and :maximize accept only one argument +Optimization1.bpl(21,11): Error: attributes :minimize and :maximize accept only one argument +4 name resolution errors detected in Optimization1.bpl diff --git a/Test/optimization/Optimization2.bpl b/Test/optimization/Optimization2.bpl new file mode 100644 index 00000000..7d80d735 --- /dev/null +++ b/Test/optimization/Optimization2.bpl @@ -0,0 +1,12 @@ +// RUN: %boogie /noVerify /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:minimize true} true; +} + +procedure test1(n: int) +{ + assume {:maximize true} true; +} diff --git a/Test/optimization/Optimization2.bpl.expect b/Test/optimization/Optimization2.bpl.expect new file mode 100644 index 00000000..cab2fd3d --- /dev/null +++ b/Test/optimization/Optimization2.bpl.expect @@ -0,0 +1,3 @@ +Optimization2.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv +Optimization2.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv +2 type checking errors detected in Optimization2.bpl diff --git a/Test/optimization/Optimization3.bpl b/Test/optimization/Optimization3.bpl new file mode 100644 index 00000000..02499c31 --- /dev/null +++ b/Test/optimization/Optimization3.bpl @@ -0,0 +1,20 @@ +// RUN: %boogie /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0() +{ + var x: int; + + assume x < 42; + assume {:maximize x} true; + assert (exists y: int :: y < x); +} + +procedure test1() +{ + var x: int; + + assume x < 42; + assume {:maximize x} true; + assert (forall y: int :: y < x); +} diff --git a/Test/optimization/Optimization3.bpl.expect b/Test/optimization/Optimization3.bpl.expect new file mode 100644 index 00000000..6a0066fc --- /dev/null +++ b/Test/optimization/Optimization3.bpl.expect @@ -0,0 +1,31 @@ +*** MODEL +%lbl%@80 -> false +%lbl%+33 -> true +%lbl%+61 -> true +x -> 41 +tickleBool -> { + true -> true + false -> true + else -> true +} +*** END_MODEL +Optimization3.bpl(10,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization3.bpl(8,5): anon0 +*** MODEL +%lbl%@115 -> false +%lbl%+105 -> true +%lbl%+56 -> true +x@@0 -> 41 +y@@0!1!1 -> 719 +tickleBool -> { + true -> true + false -> true + else -> true +} +*** END_MODEL +Optimization3.bpl(19,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization3.bpl(17,5): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/optimization/lit.local.cfg b/Test/optimization/lit.local.cfg new file mode 100644 index 00000000..35c7e558 --- /dev/null +++ b/Test/optimization/lit.local.cfg @@ -0,0 +1,3 @@ +# Do not run tests in this directory and below +config.unsupported = True +# TODO(wuestholz): Enable these tests once we can rely on a version of Z3 that includes changeset 5948013b1b04d8529bce366c0c7b87e1d88a1827. |