From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Wed, 15 Jul 2009 21:03:41 +0000 Subject: Initial set of files. --- Test/inline/Answer | 983 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 983 insertions(+) create mode 100644 Test/inline/Answer (limited to 'Test/inline/Answer') 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; +} + + +(68,4): Error BP5003: A postcondition might not hold at this return statement. +(78,2): Related location: This is the postcondition that might not hold. +Execution trace: + (19,0): anon0 + (22,0): inline$find$0$Entry + (28,0): inline$find$0$anon0 + (38,0): inline$find$0$anon4_LoopBody + (42,0): inline$check$0$Entry + (57,0): inline$check$0$anon4_Else + (62,0): inline$check$0$anon3 + (65,0): inline$check$0$Return +(100,4): Error BP5001: This assertion might not hold. +Execution trace: + (19,0): anon0 + (22,0): inline$find$0$Entry + (28,0): inline$find$0$anon0 + (38,0): inline$find$0$anon4_LoopBody + (42,0): inline$check$0$Entry + (52,0): inline$check$0$anon4_Then + (65,0): inline$check$0$Return + (73,0): inline$find$0$anon5_Then + (87,0): inline$find$0$anon3 + (90,0): inline$find$0$Return + (95,0): anon0$1 + (98,0): anon3_Then +(50,4): Error BP5003: A postcondition might not hold at this return statement. +(78,2): Related location: This is the postcondition that might not hold. +Execution trace: + (10,0): anon0 + (20,0): anon4_LoopBody + (24,0): inline$check$0$Entry + (39,0): inline$check$0$anon4_Else + (44,0): inline$check$0$anon3 + (47,0): inline$check$0$Return +(99,0): Error BP5003: A postcondition might not hold at this return statement. +(78,2): Related location: This is the postcondition that might not hold. +Execution trace: + (85,0): anon0 + (93,0): anon4_Else + (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 -- cgit v1.2.3