From 24900726a3934752401ff481ac773b2b1ddcb7d0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 18:35:08 +0100 Subject: Enable the Constant propagation tests as lit tests. --- Test/aitest0/Answer | 88 +++++++++++++++--------------- Test/aitest0/Intervals.bpl | 2 + Test/aitest0/Intervals.bpl.expect | 57 ++++++++++++++++++++ Test/aitest0/constants.bpl | 2 + Test/aitest0/constants.bpl.expect | 111 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 216 insertions(+), 44 deletions(-) create mode 100644 Test/aitest0/Intervals.bpl.expect create mode 100644 Test/aitest0/constants.bpl.expect (limited to 'Test/aitest0') diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer index cc518d1b..1d19f568 100644 --- a/Test/aitest0/Answer +++ b/Test/aitest0/Answer @@ -109,60 +109,60 @@ implementation Evaluate() Boogie program verifier finished with 0 verified, 0 errors -Intervals.bpl(62,3): Error BP5001: This assertion might not hold. +Intervals.bpl(64,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(57,5): anon0 - Intervals.bpl(58,3): anon3_LoopHead - Intervals.bpl(58,3): anon3_LoopDone -Intervals.bpl(73,3): Error BP5001: This assertion might not hold. + Intervals.bpl(59,5): anon0 + Intervals.bpl(60,3): anon3_LoopHead + Intervals.bpl(60,3): anon3_LoopDone +Intervals.bpl(75,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(68,5): anon0 - Intervals.bpl(69,3): anon3_LoopHead - Intervals.bpl(69,3): anon3_LoopDone -Intervals.bpl(92,3): Error BP5001: This assertion might not hold. + Intervals.bpl(70,5): anon0 + Intervals.bpl(71,3): anon3_LoopHead + Intervals.bpl(71,3): anon3_LoopDone +Intervals.bpl(94,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(87,5): anon0 - Intervals.bpl(88,3): loop_head - Intervals.bpl(91,3): after_loop -Intervals.bpl(138,3): Error BP5001: This assertion might not hold. + Intervals.bpl(89,5): anon0 + Intervals.bpl(90,3): loop_head + Intervals.bpl(93,3): after_loop +Intervals.bpl(140,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(133,5): anon0 - Intervals.bpl(134,3): anon3_LoopHead - Intervals.bpl(134,3): anon3_LoopDone -Intervals.bpl(149,3): Error BP5001: This assertion might not hold. + Intervals.bpl(135,5): anon0 + Intervals.bpl(136,3): anon3_LoopHead + Intervals.bpl(136,3): anon3_LoopDone +Intervals.bpl(151,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(144,5): anon0 - Intervals.bpl(145,3): anon3_LoopHead - Intervals.bpl(145,3): anon3_LoopDone -Intervals.bpl(200,3): Error BP5001: This assertion might not hold. + Intervals.bpl(146,5): anon0 + Intervals.bpl(147,3): anon3_LoopHead + Intervals.bpl(147,3): anon3_LoopDone +Intervals.bpl(202,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(190,8): anon0 - Intervals.bpl(191,3): anon4_LoopHead - Intervals.bpl(191,3): anon4_LoopDone -Intervals.bpl(238,3): Error BP5001: This assertion might not hold. + Intervals.bpl(192,8): anon0 + Intervals.bpl(193,3): anon4_LoopHead + Intervals.bpl(193,3): anon4_LoopDone +Intervals.bpl(240,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(233,5): anon0 - Intervals.bpl(234,3): anon3_LoopHead - Intervals.bpl(234,3): anon3_LoopDone -Intervals.bpl(250,3): Error BP5001: This assertion might not hold. + Intervals.bpl(235,5): anon0 + Intervals.bpl(236,3): anon3_LoopHead + Intervals.bpl(236,3): anon3_LoopDone +Intervals.bpl(252,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(244,8): anon0 - Intervals.bpl(245,3): anon3_LoopHead - Intervals.bpl(245,3): anon3_LoopDone -Intervals.bpl(261,3): Error BP5001: This assertion might not hold. + Intervals.bpl(246,8): anon0 + Intervals.bpl(247,3): anon3_LoopHead + Intervals.bpl(247,3): anon3_LoopDone +Intervals.bpl(263,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(256,5): anon0 - Intervals.bpl(257,3): anon3_LoopHead - Intervals.bpl(257,3): anon3_LoopDone -Intervals.bpl(283,3): Error BP5001: This assertion might not hold. + Intervals.bpl(258,5): anon0 + Intervals.bpl(259,3): anon3_LoopHead + Intervals.bpl(259,3): anon3_LoopDone +Intervals.bpl(285,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(278,5): anon0 - Intervals.bpl(279,3): anon3_LoopHead - Intervals.bpl(279,3): anon3_LoopDone -Intervals.bpl(305,3): Error BP5001: This assertion might not hold. + Intervals.bpl(280,5): anon0 + Intervals.bpl(281,3): anon3_LoopHead + Intervals.bpl(281,3): anon3_LoopDone +Intervals.bpl(307,3): Error BP5001: This assertion might not hold. Execution trace: - Intervals.bpl(300,5): anon0 - Intervals.bpl(301,3): anon3_LoopHead - Intervals.bpl(301,3): anon3_LoopDone + Intervals.bpl(302,5): anon0 + Intervals.bpl(303,3): anon3_LoopHead + Intervals.bpl(303,3): anon3_LoopDone Boogie program verifier finished with 16 verified, 11 errors diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl index c769645f..b9ff8269 100644 --- a/Test/aitest0/Intervals.bpl +++ b/Test/aitest0/Intervals.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j %s > %t +// RUN: %diff %s.expect %t const N: int; axiom 0 <= N; diff --git a/Test/aitest0/Intervals.bpl.expect b/Test/aitest0/Intervals.bpl.expect new file mode 100644 index 00000000..a0769ec5 --- /dev/null +++ b/Test/aitest0/Intervals.bpl.expect @@ -0,0 +1,57 @@ +Intervals.bpl(64,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(59,5): anon0 + Intervals.bpl(60,3): anon3_LoopHead + Intervals.bpl(60,3): anon3_LoopDone +Intervals.bpl(75,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(70,5): anon0 + Intervals.bpl(71,3): anon3_LoopHead + Intervals.bpl(71,3): anon3_LoopDone +Intervals.bpl(94,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(89,5): anon0 + Intervals.bpl(90,3): loop_head + Intervals.bpl(93,3): after_loop +Intervals.bpl(140,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(135,5): anon0 + Intervals.bpl(136,3): anon3_LoopHead + Intervals.bpl(136,3): anon3_LoopDone +Intervals.bpl(151,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(146,5): anon0 + Intervals.bpl(147,3): anon3_LoopHead + Intervals.bpl(147,3): anon3_LoopDone +Intervals.bpl(202,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(192,8): anon0 + Intervals.bpl(193,3): anon4_LoopHead + Intervals.bpl(193,3): anon4_LoopDone +Intervals.bpl(240,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(235,5): anon0 + Intervals.bpl(236,3): anon3_LoopHead + Intervals.bpl(236,3): anon3_LoopDone +Intervals.bpl(252,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(246,8): anon0 + Intervals.bpl(247,3): anon3_LoopHead + Intervals.bpl(247,3): anon3_LoopDone +Intervals.bpl(263,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(258,5): anon0 + Intervals.bpl(259,3): anon3_LoopHead + Intervals.bpl(259,3): anon3_LoopDone +Intervals.bpl(285,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(280,5): anon0 + Intervals.bpl(281,3): anon3_LoopHead + Intervals.bpl(281,3): anon3_LoopDone +Intervals.bpl(307,3): Error BP5001: This assertion might not hold. +Execution trace: + Intervals.bpl(302,5): anon0 + Intervals.bpl(303,3): anon3_LoopHead + Intervals.bpl(303,3): anon3_LoopDone + +Boogie program verifier finished with 16 verified, 11 errors diff --git a/Test/aitest0/constants.bpl b/Test/aitest0/constants.bpl index 3a47bfcd..dbdc32d6 100644 --- a/Test/aitest0/constants.bpl +++ b/Test/aitest0/constants.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t // Test the constant propagation AI var GlobalFlag : bool; diff --git a/Test/aitest0/constants.bpl.expect b/Test/aitest0/constants.bpl.expect new file mode 100644 index 00000000..b23f9938 --- /dev/null +++ b/Test/aitest0/constants.bpl.expect @@ -0,0 +1,111 @@ +var GlobalFlag: bool; + +const A: int; + +const B: int; + +const C: int; + +procedure Join(b: bool); + modifies GlobalFlag; + + + +implementation Join(b: bool) +{ + var x: int; + var y: int; + var z: int; + + start: + assume {:inferred} true; + GlobalFlag := true; + x := 3; + y := 4; + z := x + y; + assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7; + goto Then, Else; + + Else: + assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7; + assume b <==> false; + y := 4; + assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7 && !b; + goto join; + + join: + assume {:inferred} GlobalFlag && 3 <= x && x < 5 && y == 4 && z == 7; + assert y == 4; + assert z == 7; + assert GlobalFlag <==> true; + assume {:inferred} GlobalFlag && 3 <= x && x < 5 && y == 4 && z == 7; + return; + + Then: + assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7; + assume b <==> true; + x := x + 1; + assume {:inferred} GlobalFlag && x == 4 && y == 4 && z == 7 && b; + goto join; +} + + + +procedure Loop(); + + + +implementation Loop() +{ + var c: int; + var i: int; + + start: + assume {:inferred} true; + c := 0; + i := 0; + assume {:inferred} c == 0 && i == 0; + goto test; + + test: // cut point + assume {:inferred} c == 0 && 0 <= i && i < 11; + assume {:inferred} c == 0 && 0 <= i && i < 11; + goto Then, Else; + + Else: + assume {:inferred} c == 0 && 0 <= i && i < 11; + assume {:inferred} c == 0 && 0 <= i && i < 11; + return; + + Then: + assume {:inferred} c == 0 && 0 <= i && i < 11; + assume i < 10; + i := i + 1; + assume {:inferred} c == 0 && 1 <= i && i < 11; + goto test; +} + + + +procedure Evaluate(); + + + +implementation Evaluate() +{ + var i: int; + + start: + assume {:inferred} true; + i := 5; + i := 3 * i + 1; + i := 3 * (i + 1); + i := 1 + 3 * i; + i := (i + 1) * 3; + assume {:inferred} i == 465; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors -- cgit v1.2.3