Enable the Constant propagation tests as lit tests.

5 files changed, 216 insertions, 44 deletions

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