diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/inline/Answer | |
Initial set of files.
Diffstat (limited to 'Test/inline/Answer')
| -rw-r--r-- | Test/inline/Answer | 983 |
1 files changed, 983 insertions, 0 deletions
diff --git a/Test/inline/Answer b/Test/inline/Answer new file mode 100644 index 00000000..39d5a5b4 --- /dev/null +++ b/Test/inline/Answer @@ -0,0 +1,983 @@ +-------------------- test1.bpl --------------------
+
+procedure Main();
+
+
+
+implementation Main()
+{
+ var x: int;
+ var y: int;
+
+ anon0:
+ x := 1;
+ y := 0;
+ call x := inc(x, 5);
+ call y := incdec(x, 2);
+ assert x - 1 == y;
+ return;
+}
+
+
+
+procedure {:inline 1} incdec(x: int, y: int) returns (z: int);
+ ensures z == x + 1 - y;
+
+
+
+implementation incdec(x: int, y: int) returns (z: int)
+{
+
+ anon0:
+ z := x;
+ z := x + 1;
+ call z := dec(z, y);
+ return;
+}
+
+
+
+procedure {:inline 1} inc(x: int, i: int) returns (y: int);
+ ensures y == x + i;
+
+
+
+implementation inc(x: int, i: int) returns (y: int)
+{
+
+ anon0:
+ y := x;
+ y := x + i;
+ return;
+}
+
+
+
+procedure {:inline 1} dec(x: int, i: int) returns (y: int);
+ ensures y == x - i;
+
+
+
+implementation dec(x: int, i: int) returns (y: int)
+{
+
+ anon0:
+ y := x;
+ y := x - i;
+ return;
+}
+
+
+after inlining procedure calls
+procedure Main();
+
+
+implementation Main()
+{
+ var x: int;
+ var y: int;
+ var inline$inc$0$x: int;
+ var inline$inc$0$i: int;
+ var inline$inc$0$y: int;
+ var inline$incdec$0$x: int;
+ var inline$incdec$0$y: int;
+ var inline$incdec$0$z: int;
+ var inline$dec$0$x: int;
+ var inline$dec$0$i: int;
+ var inline$dec$0$y: int;
+
+ anon0:
+ x := 1;
+ y := 0;
+ goto inline$inc$0$Entry;
+
+ inline$inc$0$Entry:
+ inline$inc$0$x := x;
+ inline$inc$0$i := 5;
+ goto inline$inc$0$anon0;
+
+ inline$inc$0$anon0:
+ inline$inc$0$y := inline$inc$0$x;
+ inline$inc$0$y := inline$inc$0$x + inline$inc$0$i;
+ goto inline$inc$0$Return;
+
+ inline$inc$0$Return:
+ assert inline$inc$0$y == inline$inc$0$x + inline$inc$0$i;
+ x := inline$inc$0$y;
+ goto anon0$1;
+
+ anon0$1:
+ goto inline$incdec$0$Entry;
+
+ inline$incdec$0$Entry:
+ inline$incdec$0$x := x;
+ inline$incdec$0$y := 2;
+ goto inline$incdec$0$anon0;
+
+ inline$incdec$0$anon0:
+ inline$incdec$0$z := inline$incdec$0$x;
+ inline$incdec$0$z := inline$incdec$0$x + 1;
+ goto inline$dec$0$Entry;
+
+ inline$dec$0$Entry:
+ inline$dec$0$x := inline$incdec$0$z;
+ inline$dec$0$i := inline$incdec$0$y;
+ goto inline$dec$0$anon0;
+
+ inline$dec$0$anon0:
+ inline$dec$0$y := inline$dec$0$x;
+ inline$dec$0$y := inline$dec$0$x - inline$dec$0$i;
+ goto inline$dec$0$Return;
+
+ inline$dec$0$Return:
+ assert inline$dec$0$y == inline$dec$0$x - inline$dec$0$i;
+ inline$incdec$0$z := inline$dec$0$y;
+ goto inline$incdec$0$anon0$1;
+
+ inline$incdec$0$anon0$1:
+ goto inline$incdec$0$Return;
+
+ inline$incdec$0$Return:
+ assert inline$incdec$0$z == inline$incdec$0$x + 1 - inline$incdec$0$y;
+ y := inline$incdec$0$z;
+ goto anon0$2;
+
+ anon0$2:
+ assert x - 1 == y;
+ return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 1} incdec(x: int, y: int) returns (z: int);
+ ensures z == x + 1 - y;
+
+
+implementation incdec(x: int, y: int) returns (z: int)
+{
+ var inline$dec$0$x: int;
+ var inline$dec$0$i: int;
+ var inline$dec$0$y: int;
+
+ anon0:
+ z := x;
+ z := x + 1;
+ goto inline$dec$0$Entry;
+
+ inline$dec$0$Entry:
+ inline$dec$0$x := z;
+ inline$dec$0$i := y;
+ goto inline$dec$0$anon0;
+
+ inline$dec$0$anon0:
+ inline$dec$0$y := inline$dec$0$x;
+ inline$dec$0$y := inline$dec$0$x - inline$dec$0$i;
+ goto inline$dec$0$Return;
+
+ inline$dec$0$Return:
+ assert inline$dec$0$y == inline$dec$0$x - inline$dec$0$i;
+ z := inline$dec$0$y;
+ goto anon0$1;
+
+ anon0$1:
+ return;
+}
+
+
+
+Boogie program verifier finished with 4 verified, 0 errors
+-------------------- test2.bpl --------------------
+
+var glb: int;
+
+procedure calculate();
+ modifies glb;
+
+
+
+implementation calculate()
+{
+ var x: int;
+ var y: int;
+
+ anon0:
+ y := 5;
+ call x := increase(y);
+ return;
+}
+
+
+
+procedure {:inline 1} increase(i: int) returns (k: int);
+ modifies glb;
+
+
+
+implementation increase(i: int) returns (k: int)
+{
+ var j: int;
+
+ anon0:
+ j := i;
+ j := j + 1;
+ glb := glb + j;
+ k := j;
+ return;
+}
+
+
+after inlining procedure calls
+procedure calculate();
+ modifies glb;
+
+
+implementation calculate()
+{
+ var x: int;
+ var y: int;
+ var inline$increase$0$j: int;
+ var inline$increase$0$i: int;
+ var inline$increase$0$k: int;
+ var inline$increase$0$glb: int;
+
+ anon0:
+ y := 5;
+ goto inline$increase$0$Entry;
+
+ inline$increase$0$Entry:
+ inline$increase$0$i := y;
+ inline$increase$0$glb := glb;
+ goto inline$increase$0$anon0;
+
+ inline$increase$0$anon0:
+ inline$increase$0$j := inline$increase$0$i;
+ inline$increase$0$j := inline$increase$0$j + 1;
+ glb := glb + inline$increase$0$j;
+ inline$increase$0$k := inline$increase$0$j;
+ goto inline$increase$0$Return;
+
+ inline$increase$0$Return:
+ x := inline$increase$0$k;
+ goto anon0$1;
+
+ anon0$1:
+ return;
+}
+
+
+
+Boogie program verifier finished with 2 verified, 0 errors
+-------------------- test3.bpl --------------------
+
+var glb: int;
+
+procedure recursivetest();
+ modifies glb;
+
+
+
+implementation recursivetest()
+{
+
+ anon0:
+ glb := 5;
+ call glb := recursive(glb);
+ return;
+}
+
+
+
+procedure {:inline 3} recursive(x: int) returns (y: int);
+
+
+
+implementation recursive(x: int) returns (y: int)
+{
+ var k: int;
+
+ anon0:
+ goto anon3_Then, anon3_Else;
+
+ anon3_Then:
+ assume x == 0;
+ y := 1;
+ return;
+
+ anon3_Else:
+ assume x != 0;
+ goto anon2;
+
+ anon2:
+ call k := recursive(x - 1);
+ y := y + k;
+ return;
+}
+
+
+after inlining procedure calls
+procedure recursivetest();
+ modifies glb;
+
+
+implementation recursivetest()
+{
+ var inline$recursive$0$k: int;
+ var inline$recursive$0$x: int;
+ var inline$recursive$0$y: int;
+ var inline$recursive$1$k: int;
+ var inline$recursive$1$x: int;
+ var inline$recursive$1$y: int;
+ var inline$recursive$2$k: int;
+ var inline$recursive$2$x: int;
+ var inline$recursive$2$y: int;
+
+ anon0:
+ glb := 5;
+ goto inline$recursive$0$Entry;
+
+ inline$recursive$0$Entry:
+ inline$recursive$0$x := glb;
+ goto inline$recursive$0$anon0;
+
+ inline$recursive$0$anon0:
+ goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;
+
+ inline$recursive$0$anon3_Then:
+ assume inline$recursive$0$x == 0;
+ inline$recursive$0$y := 1;
+ goto inline$recursive$0$Return;
+
+ inline$recursive$0$anon3_Else:
+ assume inline$recursive$0$x != 0;
+ goto inline$recursive$0$anon2;
+
+ inline$recursive$0$anon2:
+ goto inline$recursive$1$Entry;
+
+ inline$recursive$1$Entry:
+ inline$recursive$1$x := inline$recursive$0$x - 1;
+ goto inline$recursive$1$anon0;
+
+ inline$recursive$1$anon0:
+ goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;
+
+ inline$recursive$1$anon3_Then:
+ assume inline$recursive$1$x == 0;
+ inline$recursive$1$y := 1;
+ goto inline$recursive$1$Return;
+
+ inline$recursive$1$anon3_Else:
+ assume inline$recursive$1$x != 0;
+ goto inline$recursive$1$anon2;
+
+ inline$recursive$1$anon2:
+ goto inline$recursive$2$Entry;
+
+ inline$recursive$2$Entry:
+ inline$recursive$2$x := inline$recursive$1$x - 1;
+ goto inline$recursive$2$anon0;
+
+ inline$recursive$2$anon0:
+ goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;
+
+ inline$recursive$2$anon3_Then:
+ assume inline$recursive$2$x == 0;
+ inline$recursive$2$y := 1;
+ goto inline$recursive$2$Return;
+
+ inline$recursive$2$anon3_Else:
+ assume inline$recursive$2$x != 0;
+ goto inline$recursive$2$anon2;
+
+ inline$recursive$2$anon2:
+ call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);
+ inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;
+ goto inline$recursive$2$Return;
+
+ inline$recursive$2$Return:
+ inline$recursive$1$k := inline$recursive$2$y;
+ goto inline$recursive$1$anon2$1;
+
+ inline$recursive$1$anon2$1:
+ inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k;
+ goto inline$recursive$1$Return;
+
+ inline$recursive$1$Return:
+ inline$recursive$0$k := inline$recursive$1$y;
+ goto inline$recursive$0$anon2$1;
+
+ inline$recursive$0$anon2$1:
+ inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k;
+ goto inline$recursive$0$Return;
+
+ inline$recursive$0$Return:
+ glb := inline$recursive$0$y;
+ goto anon0$1;
+
+ anon0$1:
+ return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 3} recursive(x: int) returns (y: int);
+
+
+implementation recursive(x: int) returns (y: int)
+{
+ var k: int;
+ var inline$recursive$0$k: int;
+ var inline$recursive$0$x: int;
+ var inline$recursive$0$y: int;
+ var inline$recursive$1$k: int;
+ var inline$recursive$1$x: int;
+ var inline$recursive$1$y: int;
+ var inline$recursive$2$k: int;
+ var inline$recursive$2$x: int;
+ var inline$recursive$2$y: int;
+
+ anon0:
+ goto anon3_Then, anon3_Else;
+
+ anon3_Then:
+ assume x == 0;
+ y := 1;
+ return;
+
+ anon3_Else:
+ assume x != 0;
+ goto anon2;
+
+ anon2:
+ goto inline$recursive$0$Entry;
+
+ inline$recursive$0$Entry:
+ inline$recursive$0$x := x - 1;
+ goto inline$recursive$0$anon0;
+
+ inline$recursive$0$anon0:
+ goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;
+
+ inline$recursive$0$anon3_Then:
+ assume inline$recursive$0$x == 0;
+ inline$recursive$0$y := 1;
+ goto inline$recursive$0$Return;
+
+ inline$recursive$0$anon3_Else:
+ assume inline$recursive$0$x != 0;
+ goto inline$recursive$0$anon2;
+
+ inline$recursive$0$anon2:
+ goto inline$recursive$1$Entry;
+
+ inline$recursive$1$Entry:
+ inline$recursive$1$x := inline$recursive$0$x - 1;
+ goto inline$recursive$1$anon0;
+
+ inline$recursive$1$anon0:
+ goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;
+
+ inline$recursive$1$anon3_Then:
+ assume inline$recursive$1$x == 0;
+ inline$recursive$1$y := 1;
+ goto inline$recursive$1$Return;
+
+ inline$recursive$1$anon3_Else:
+ assume inline$recursive$1$x != 0;
+ goto inline$recursive$1$anon2;
+
+ inline$recursive$1$anon2:
+ goto inline$recursive$2$Entry;
+
+ inline$recursive$2$Entry:
+ inline$recursive$2$x := inline$recursive$1$x - 1;
+ goto inline$recursive$2$anon0;
+
+ inline$recursive$2$anon0:
+ goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;
+
+ inline$recursive$2$anon3_Then:
+ assume inline$recursive$2$x == 0;
+ inline$recursive$2$y := 1;
+ goto inline$recursive$2$Return;
+
+ inline$recursive$2$anon3_Else:
+ assume inline$recursive$2$x != 0;
+ goto inline$recursive$2$anon2;
+
+ inline$recursive$2$anon2:
+ call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);
+ inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;
+ goto inline$recursive$2$Return;
+
+ inline$recursive$2$Return:
+ inline$recursive$1$k := inline$recursive$2$y;
+ goto inline$recursive$1$anon2$1;
+
+ inline$recursive$1$anon2$1:
+ inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k;
+ goto inline$recursive$1$Return;
+
+ inline$recursive$1$Return:
+ inline$recursive$0$k := inline$recursive$1$y;
+ goto inline$recursive$0$anon2$1;
+
+ inline$recursive$0$anon2$1:
+ inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k;
+ goto inline$recursive$0$Return;
+
+ inline$recursive$0$Return:
+ k := inline$recursive$0$y;
+ goto anon2$1;
+
+ anon2$1:
+ y := y + k;
+ return;
+}
+
+
+
+Boogie program verifier finished with 2 verified, 0 errors
+-------------------- test4.bpl --------------------
+
+procedure main(x: int);
+
+
+
+implementation main(x: int)
+{
+ var A: [int]int;
+ var i: int;
+ var b: bool;
+ var size: int;
+
+ anon0:
+ call i, b := find(A, size, x);
+ goto anon3_Then, anon3_Else;
+
+ anon3_Then:
+ assume b;
+ assert i > 0 && A[i] == x;
+ goto anon2;
+
+ anon3_Else:
+ assume !b;
+ goto anon2;
+
+ anon2:
+ return;
+}
+
+
+
+procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);
+
+
+
+implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+{
+ var i: int;
+ var b: bool;
+
+ anon0:
+ ret := 0 - 1;
+ b := false;
+ found := b;
+ i := 0;
+ goto anon4_LoopHead;
+
+ anon4_LoopHead:
+ goto anon4_LoopDone, anon4_LoopBody;
+
+ anon4_LoopBody:
+ assume i < size;
+ call b := check(A, i, x);
+ goto anon5_Then, anon5_Else;
+
+ anon5_Then:
+ assume b;
+ ret := i;
+ found := b;
+ goto anon3;
+
+ anon5_Else:
+ assume !b;
+ goto anon4_LoopHead;
+
+ anon4_LoopDone:
+ assume i >= size;
+ goto anon3;
+
+ anon3:
+ return;
+}
+
+
+
+procedure {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool);
+ requires i >= 0;
+ ensures old(A[i]) > c ==> ret == true;
+
+
+
+implementation check(A: [int]int, i: int, c: int) returns (ret: bool)
+{
+
+ anon0:
+ goto anon4_Then, anon4_Else;
+
+ anon4_Then:
+ assume A[i] == c;
+ ret := true;
+ goto anon3;
+
+ anon4_Else:
+ assume A[i] != c;
+ ret := false;
+ goto anon3;
+
+ anon3:
+ return;
+}
+
+
+after inlining procedure calls
+procedure main(x: int);
+
+
+implementation main(x: int)
+{
+ var A: [int]int;
+ var i: int;
+ var b: bool;
+ var size: int;
+ var inline$find$0$i: int;
+ var inline$find$0$b: bool;
+ var inline$find$0$A: [int]int;
+ var inline$find$0$size: int;
+ var inline$find$0$x: int;
+ var inline$find$0$ret: int;
+ var inline$find$0$found: bool;
+ var inline$check$0$A: [int]int;
+ var inline$check$0$i: int;
+ var inline$check$0$c: int;
+ var inline$check$0$ret: bool;
+
+ anon0:
+ goto inline$find$0$Entry;
+
+ inline$find$0$Entry:
+ inline$find$0$A := A;
+ inline$find$0$size := size;
+ inline$find$0$x := x;
+ goto inline$find$0$anon0;
+
+ inline$find$0$anon0:
+ inline$find$0$ret := 0 - 1;
+ inline$find$0$b := false;
+ inline$find$0$found := inline$find$0$b;
+ inline$find$0$i := 0;
+ goto inline$find$0$anon4_LoopHead;
+
+ inline$find$0$anon4_LoopHead:
+ goto inline$find$0$anon4_LoopDone, inline$find$0$anon4_LoopBody;
+
+ inline$find$0$anon4_LoopBody:
+ assume inline$find$0$i < inline$find$0$size;
+ goto inline$check$0$Entry;
+
+ inline$check$0$Entry:
+ inline$check$0$A := inline$find$0$A;
+ inline$check$0$i := inline$find$0$i;
+ inline$check$0$c := inline$find$0$x;
+ assert inline$check$0$i >= 0;
+ goto inline$check$0$anon0;
+
+ inline$check$0$anon0:
+ goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;
+
+ inline$check$0$anon4_Then:
+ assume inline$check$0$A[inline$check$0$i] == inline$check$0$c;
+ inline$check$0$ret := true;
+ goto inline$check$0$anon3;
+
+ inline$check$0$anon4_Else:
+ assume inline$check$0$A[inline$check$0$i] != inline$check$0$c;
+ inline$check$0$ret := false;
+ goto inline$check$0$anon3;
+
+ inline$check$0$anon3:
+ goto inline$check$0$Return;
+
+ inline$check$0$Return:
+ assert inline$check$0$A[inline$check$0$i] > inline$check$0$c ==> (inline$check$0$ret <==> true);
+ inline$find$0$b := inline$check$0$ret;
+ goto inline$find$0$anon4_LoopBody$1;
+
+ inline$find$0$anon4_LoopBody$1:
+ goto inline$find$0$anon5_Then, inline$find$0$anon5_Else;
+
+ inline$find$0$anon5_Then:
+ assume inline$find$0$b;
+ inline$find$0$ret := inline$find$0$i;
+ inline$find$0$found := inline$find$0$b;
+ goto inline$find$0$anon3;
+
+ inline$find$0$anon5_Else:
+ assume !inline$find$0$b;
+ goto inline$find$0$anon4_LoopHead;
+
+ inline$find$0$anon4_LoopDone:
+ assume inline$find$0$i >= inline$find$0$size;
+ goto inline$find$0$anon3;
+
+ inline$find$0$anon3:
+ goto inline$find$0$Return;
+
+ inline$find$0$Return:
+ i := inline$find$0$ret;
+ b := inline$find$0$found;
+ goto anon0$1;
+
+ anon0$1:
+ goto anon3_Then, anon3_Else;
+
+ anon3_Then:
+ assume b;
+ assert i > 0 && A[i] == x;
+ goto anon2;
+
+ anon3_Else:
+ assume !b;
+ goto anon2;
+
+ anon2:
+ return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);
+
+
+implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+{
+ var i: int;
+ var b: bool;
+ var inline$check$0$A: [int]int;
+ var inline$check$0$i: int;
+ var inline$check$0$c: int;
+ var inline$check$0$ret: bool;
+
+ anon0:
+ ret := 0 - 1;
+ b := false;
+ found := b;
+ i := 0;
+ goto anon4_LoopHead;
+
+ anon4_LoopHead:
+ goto anon4_LoopDone, anon4_LoopBody;
+
+ anon4_LoopBody:
+ assume i < size;
+ goto inline$check$0$Entry;
+
+ inline$check$0$Entry:
+ inline$check$0$A := A;
+ inline$check$0$i := i;
+ inline$check$0$c := x;
+ assert inline$check$0$i >= 0;
+ goto inline$check$0$anon0;
+
+ inline$check$0$anon0:
+ goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;
+
+ inline$check$0$anon4_Then:
+ assume inline$check$0$A[inline$check$0$i] == inline$check$0$c;
+ inline$check$0$ret := true;
+ goto inline$check$0$anon3;
+
+ inline$check$0$anon4_Else:
+ assume inline$check$0$A[inline$check$0$i] != inline$check$0$c;
+ inline$check$0$ret := false;
+ goto inline$check$0$anon3;
+
+ inline$check$0$anon3:
+ goto inline$check$0$Return;
+
+ inline$check$0$Return:
+ assert inline$check$0$A[inline$check$0$i] > inline$check$0$c ==> (inline$check$0$ret <==> true);
+ b := inline$check$0$ret;
+ goto anon4_LoopBody$1;
+
+ anon4_LoopBody$1:
+ goto anon5_Then, anon5_Else;
+
+ anon5_Then:
+ assume b;
+ ret := i;
+ found := b;
+ goto anon3;
+
+ anon5_Else:
+ assume !b;
+ goto anon4_LoopHead;
+
+ anon4_LoopDone:
+ assume i >= size;
+ goto anon3;
+
+ anon3:
+ return;
+}
+
+
+<console>(68,4): Error BP5003: A postcondition might not hold at this return statement.
+<console>(78,2): Related location: This is the postcondition that might not hold.
+Execution trace:
+ <console>(19,0): anon0
+ <console>(22,0): inline$find$0$Entry
+ <console>(28,0): inline$find$0$anon0
+ <console>(38,0): inline$find$0$anon4_LoopBody
+ <console>(42,0): inline$check$0$Entry
+ <console>(57,0): inline$check$0$anon4_Else
+ <console>(62,0): inline$check$0$anon3
+ <console>(65,0): inline$check$0$Return
+<console>(100,4): Error BP5001: This assertion might not hold.
+Execution trace:
+ <console>(19,0): anon0
+ <console>(22,0): inline$find$0$Entry
+ <console>(28,0): inline$find$0$anon0
+ <console>(38,0): inline$find$0$anon4_LoopBody
+ <console>(42,0): inline$check$0$Entry
+ <console>(52,0): inline$check$0$anon4_Then
+ <console>(65,0): inline$check$0$Return
+ <console>(73,0): inline$find$0$anon5_Then
+ <console>(87,0): inline$find$0$anon3
+ <console>(90,0): inline$find$0$Return
+ <console>(95,0): anon0$1
+ <console>(98,0): anon3_Then
+<console>(50,4): Error BP5003: A postcondition might not hold at this return statement.
+<console>(78,2): Related location: This is the postcondition that might not hold.
+Execution trace:
+ <console>(10,0): anon0
+ <console>(20,0): anon4_LoopBody
+ <console>(24,0): inline$check$0$Entry
+ <console>(39,0): inline$check$0$anon4_Else
+ <console>(44,0): inline$check$0$anon3
+ <console>(47,0): inline$check$0$Return
+<console>(99,0): Error BP5003: A postcondition might not hold at this return statement.
+<console>(78,2): Related location: This is the postcondition that might not hold.
+Execution trace:
+ <console>(85,0): anon0
+ <console>(93,0): anon4_Else
+ <console>(98,0): anon3
+
+Boogie program verifier finished with 0 verified, 4 errors
+-------------------- test5.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+-------------------- test6.bpl --------------------
+test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo
+test6.bpl(15,22): Error: the inlined procedure is recursive, call stack: foo2 -> foo3 -> foo1 -> foo2
+test6.bpl(22,22): Error: the inlined procedure is recursive, call stack: foo3 -> foo1 -> foo2 -> foo3
+test6.bpl(8,22): Error: the inlined procedure is recursive, call stack: foo1 -> foo2 -> foo3 -> foo1
+test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo
+test6.bpl(8,22): Error: the inlined procedure is recursive, call stack: foo1 -> foo2 -> foo3 -> foo1
+6 type checking errors detected in test6.bpl
+-------------------- expansion.bpl --------------------
+expansion.bpl(29,14): Error: invalid type for argument 0 in application of foo1: bool (expected: int)
+expansion.bpl(13,16): Error: expansion: {:inline ...} expects either true or false as the argument
+expansion.bpl(14,22): Error: expansion: identifier was not quantified over
+expansion.bpl(15,22): Error: expansion: identifier was not quantified over
+expansion.bpl(16,22): Error: expansion: more variables quantified over, than used in function
+expansion.bpl(18,21): Error: expansion: axiom to be expanded must have form (forall VARS :: f(VARS) == expr(VARS))
+expansion.bpl(19,53): Error: expansion: only identifiers supported as function arguments
+expansion.bpl(33,22): Error: expansion: an identifier was used more than once
+8 type checking errors detected in expansion.bpl
+-------------------- expansion3.bpl --------------------
+*** detected expansion loop on foo3
+*** detected expansion loop on foo3
+*** detected expansion loop on foo3
+*** more than one possible expansion for x1
+expansion3.bpl(18,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ expansion3.bpl(18,3): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+-------------------- Elevator.bpl --------------------
+Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Elevator.bpl(15,3): anon0
+ Elevator.bpl(68,23): inline$Initialize$0$Entry
+ Elevator.bpl(71,13): inline$Initialize$0$anon0
+ Elevator.bpl(68,23): inline$Initialize$0$Return
+ Elevator.bpl(15,3): anon0$1
+ Elevator.bpl(16,3): anon10_LoopHead
+ Elevator.bpl(19,5): anon10_LoopBody
+ Elevator.bpl(19,5): anon11_Else
+ Elevator.bpl(19,5): anon12_Else
+ Elevator.bpl(24,7): anon13_Then
+ Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry
+ Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
+ Elevator.bpl(94,23): inline$MoveDown_Error$0$Return
+ Elevator.bpl(24,7): anon13_Then$1
+
+Boogie program verifier finished with 1 verified, 1 error
+-------------------- expansion2.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+---------- EXPANSION2.SX: 0
+
+---------- EXPANSION2.SX: 0
+-------------------- expansion4.bpl --------------------
+
+Boogie program verifier finished with 3 verified, 0 errors
+-------------------- fundef.bpl --------------------
+
+function {:inline true} foo(x: int) returns (bool)
+{
+ x > 0
+}
+
+function {:inline false} foo2(x: int) returns (bool);
+
+// autogenerated definition axiom
+axiom (forall x: int :: {:inline false} { foo2(x):bool } foo2(x):bool == (x > 0));
+
+function foo3(x: int) returns (bool);
+
+// autogenerated definition axiom
+axiom (forall x: int :: { foo3(x):bool } foo3(x):bool == (x > 0));
+
+Boogie program verifier finished with 0 verified, 0 errors
+fundef2.bpl(6,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ fundef2.bpl(5,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+-------------------- polyInline.bpl --------------------
+polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(23,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ polyInline.bpl(20,3): anon0
+polyInline.bpl(39,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ polyInline.bpl(27,3): anon0
+
+Boogie program verifier finished with 0 verified, 2 errors
+polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(23,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ polyInline.bpl(20,3): anon0
+polyInline.bpl(39,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ polyInline.bpl(27,3): anon0
+
+Boogie program verifier finished with 0 verified, 2 errors
|