summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Test/aitest0/Answer88
-rw-r--r--Test/aitest0/Intervals.bpl2
-rw-r--r--Test/aitest0/Intervals.bpl.expect57
-rw-r--r--Test/aitest0/constants.bpl2
-rw-r--r--Test/aitest0/constants.bpl.expect111
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 16:58:43 +0000