Removed Output files. These are created on a local machine when the tests are run.

1 files changed, 0 insertions, 983 deletions

diff --git a/Test/inline/Output b/Test/inline/Output
deleted file mode 100644
index 39d5a5b4..00000000
--- a/Test/inline/Output
+++ /dev/null
@@ -1,983 +0,0 @@
--------------------- 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