Enabled the inline lit tests. In order to support expansion2.bpl

we now require the OutputCheck tool. The lit.site.cfg file has
been taught to require that this tool is in the user's PATH
before testing starts.

1 files changed, 332 insertions, 0 deletions

diff --git a/Test/inline/test4.bpl.expect b/Test/inline/test4.bpl.expect
new file mode 100644
index 00000000..29f80858
--- /dev/null
+++ b/Test/inline/test4.bpl.expect
@@ -0,0 +1,332 @@
+
+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 {:partition} b;
+    assert i > 0 && A[i] == x;
+    goto anon2;
+
+  anon3_Else:
+    assume {:partition} !b;
+    goto anon2;
+
+  anon2:
+    return;
+}
+
+
+
+procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);
+
+
+
+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+{
+  var i: int;
+  var b: bool;
+
+  anon0:
+    ret := -1;
+    b := false;
+    found := b;
+    i := 0;
+    goto anon4_LoopHead;
+
+  anon4_LoopHead:
+    goto anon4_LoopDone, anon4_LoopBody;
+
+  anon4_LoopBody:
+    assume {:partition} i < size;
+    call b := check(A, i, x);
+    goto anon5_Then, anon5_Else;
+
+  anon5_Then:
+    assume {:partition} b;
+    ret := i;
+    found := b;
+    goto anon3;
+
+  anon5_Else:
+    assume {:partition} !b;
+    goto anon4_LoopHead;
+
+  anon4_LoopDone:
+    assume {:partition} size <= i;
+    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 {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool)
+{
+
+  anon0:
+    goto anon4_Then, anon4_Else;
+
+  anon4_Then:
+    assume {:partition} A[i] == c;
+    ret := true;
+    goto anon3;
+
+  anon4_Else:
+    assume {:partition} 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;
+    havoc inline$find$0$i, inline$find$0$b, inline$find$0$ret, inline$find$0$found;
+    goto inline$find$0$anon0;
+
+  inline$find$0$anon0:
+    inline$find$0$ret := -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 {:partition} 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;
+    havoc inline$check$0$ret;
+    goto inline$check$0$anon0;
+
+  inline$check$0$anon0:
+    goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;
+
+  inline$check$0$anon4_Else:
+    assume {:partition} 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$anon4_Then:
+    assume {:partition} 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$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_Else:
+    assume {:partition} !inline$find$0$b;
+    goto inline$find$0$anon4_LoopHead;
+
+  inline$find$0$anon5_Then:
+    assume {:partition} 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$anon3:
+    goto inline$find$0$Return;
+
+  inline$find$0$anon4_LoopDone:
+    assume {:partition} inline$find$0$size <= inline$find$0$i;
+    goto inline$find$0$anon3;
+
+  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_Else:
+    assume {:partition} !b;
+    goto anon2;
+
+  anon2:
+    return;
+
+  anon3_Then:
+    assume {:partition} b;
+    assert i > 0 && A[i] == x;
+    goto anon2;
+}
+
+
+after inlining procedure calls
+procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);
+
+
+implementation {:inline 1} 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 := -1;
+    b := false;
+    found := b;
+    i := 0;
+    goto anon4_LoopHead;
+
+  anon4_LoopHead:
+    goto anon4_LoopDone, anon4_LoopBody;
+
+  anon4_LoopBody:
+    assume {:partition} 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;
+    havoc inline$check$0$ret;
+    goto inline$check$0$anon0;
+
+  inline$check$0$anon0:
+    goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;
+
+  inline$check$0$anon4_Else:
+    assume {:partition} 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$anon4_Then:
+    assume {:partition} 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$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_Else:
+    assume {:partition} !b;
+    goto anon4_LoopHead;
+
+  anon5_Then:
+    assume {:partition} b;
+    ret := i;
+    found := b;
+    goto anon3;
+
+  anon3:
+    return;
+
+  anon4_LoopDone:
+    assume {:partition} size <= i;
+    goto anon3;
+}
+
+
+<console>(70,4): Error BP5003: A postcondition might not hold on this return path.
+<console>(78,2): Related location: This is the postcondition that might not hold.
+Execution trace:
+    <console>(19,0): anon0
+    <console>(29,0): inline$find$0$anon0
+    <console>(39,0): inline$find$0$anon4_LoopBody
+    <console>(43,0): inline$check$0$Entry
+    <console>(54,0): inline$check$0$anon4_Else
+    <console>(67,0): inline$check$0$Return
+<console>(109,4): Error BP5001: This assertion might not hold.
+Execution trace:
+    <console>(19,0): anon0
+    <console>(29,0): inline$find$0$anon0
+    <console>(39,0): inline$find$0$anon4_LoopBody
+    <console>(43,0): inline$check$0$Entry
+    <console>(62,0): inline$check$0$anon4_Then
+    <console>(67,0): inline$check$0$Return
+    <console>(79,0): inline$find$0$anon5_Then
+    <console>(107,0): anon3_Then
+<console>(51,4): Error BP5003: A postcondition might not hold on this return path.
+<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>(35,0): inline$check$0$anon4_Else
+    <console>(48,0): inline$check$0$Return
+<console>(99,0): Error BP5003: A postcondition might not hold on this return path.
+<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