diff options
Diffstat (limited to 'Test/aitest0/Answer')
| -rw-r--r-- | Test/aitest0/Answer | 168 |
1 files changed, 0 insertions, 168 deletions
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer deleted file mode 100644 index 1d19f568..00000000 --- a/Test/aitest0/Answer +++ /dev/null @@ -1,168 +0,0 @@ -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
-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
|