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, 579 insertions, 0 deletions

diff --git a/Test/inline/test6.bpl.expect b/Test/inline/test6.bpl.expect
new file mode 100644
index 00000000..240094e1
--- /dev/null
+++ b/Test/inline/test6.bpl.expect
@@ -0,0 +1,579 @@
+
+procedure {:inline 2} foo();
+  modifies x;
+
+
+
+implementation {:inline 2} foo()
+{
+
+  anon0:
+    x := x + 1;
+    call foo();
+    return;
+}
+
+
+
+procedure {:inline 2} foo1();
+  modifies x;
+
+
+
+implementation {:inline 2} foo1()
+{
+
+  anon0:
+    x := x + 1;
+    call foo2();
+    return;
+}
+
+
+
+procedure {:inline 2} foo2();
+  modifies x;
+
+
+
+implementation {:inline 2} foo2()
+{
+
+  anon0:
+    x := x + 1;
+    call foo3();
+    return;
+}
+
+
+
+procedure {:inline 2} foo3();
+  modifies x;
+
+
+
+implementation {:inline 2} foo3()
+{
+
+  anon0:
+    x := x + 1;
+    call foo1();
+    return;
+}
+
+
+
+var x: int;
+
+procedure bar();
+  modifies x;
+
+
+
+implementation bar()
+{
+
+  anon0:
+    call foo();
+    call foo1();
+    return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo();
+  modifies x;
+
+
+implementation {:inline 2} foo()
+{
+  var inline$foo$0$x: int;
+  var inline$foo$1$x: int;
+
+  anon0:
+    x := x + 1;
+    goto inline$foo$0$Entry;
+
+  inline$foo$0$Entry:
+    inline$foo$0$x := x;
+    goto inline$foo$0$anon0;
+
+  inline$foo$0$anon0:
+    x := x + 1;
+    goto inline$foo$1$Entry;
+
+  inline$foo$1$Entry:
+    inline$foo$1$x := x;
+    goto inline$foo$1$anon0;
+
+  inline$foo$1$anon0:
+    x := x + 1;
+    call foo();
+    goto inline$foo$1$Return;
+
+  inline$foo$1$Return:
+    goto inline$foo$0$anon0$1;
+
+  inline$foo$0$anon0$1:
+    goto inline$foo$0$Return;
+
+  inline$foo$0$Return:
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo1();
+  modifies x;
+
+
+implementation {:inline 2} foo1()
+{
+  var inline$foo2$0$x: int;
+  var inline$foo3$0$x: int;
+  var inline$foo1$0$x: int;
+  var inline$foo2$1$x: int;
+  var inline$foo3$1$x: int;
+  var inline$foo1$1$x: int;
+
+  anon0:
+    x := x + 1;
+    goto inline$foo2$0$Entry;
+
+  inline$foo2$0$Entry:
+    inline$foo2$0$x := x;
+    goto inline$foo2$0$anon0;
+
+  inline$foo2$0$anon0:
+    x := x + 1;
+    goto inline$foo3$0$Entry;
+
+  inline$foo3$0$Entry:
+    inline$foo3$0$x := x;
+    goto inline$foo3$0$anon0;
+
+  inline$foo3$0$anon0:
+    x := x + 1;
+    goto inline$foo1$0$Entry;
+
+  inline$foo1$0$Entry:
+    inline$foo1$0$x := x;
+    goto inline$foo1$0$anon0;
+
+  inline$foo1$0$anon0:
+    x := x + 1;
+    goto inline$foo2$1$Entry;
+
+  inline$foo2$1$Entry:
+    inline$foo2$1$x := x;
+    goto inline$foo2$1$anon0;
+
+  inline$foo2$1$anon0:
+    x := x + 1;
+    goto inline$foo3$1$Entry;
+
+  inline$foo3$1$Entry:
+    inline$foo3$1$x := x;
+    goto inline$foo3$1$anon0;
+
+  inline$foo3$1$anon0:
+    x := x + 1;
+    goto inline$foo1$1$Entry;
+
+  inline$foo1$1$Entry:
+    inline$foo1$1$x := x;
+    goto inline$foo1$1$anon0;
+
+  inline$foo1$1$anon0:
+    x := x + 1;
+    call foo2();
+    goto inline$foo1$1$Return;
+
+  inline$foo1$1$Return:
+    goto inline$foo3$1$anon0$1;
+
+  inline$foo3$1$anon0$1:
+    goto inline$foo3$1$Return;
+
+  inline$foo3$1$Return:
+    goto inline$foo2$1$anon0$1;
+
+  inline$foo2$1$anon0$1:
+    goto inline$foo2$1$Return;
+
+  inline$foo2$1$Return:
+    goto inline$foo1$0$anon0$1;
+
+  inline$foo1$0$anon0$1:
+    goto inline$foo1$0$Return;
+
+  inline$foo1$0$Return:
+    goto inline$foo3$0$anon0$1;
+
+  inline$foo3$0$anon0$1:
+    goto inline$foo3$0$Return;
+
+  inline$foo3$0$Return:
+    goto inline$foo2$0$anon0$1;
+
+  inline$foo2$0$anon0$1:
+    goto inline$foo2$0$Return;
+
+  inline$foo2$0$Return:
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo2();
+  modifies x;
+
+
+implementation {:inline 2} foo2()
+{
+  var inline$foo3$0$x: int;
+  var inline$foo1$0$x: int;
+  var inline$foo2$0$x: int;
+  var inline$foo3$1$x: int;
+  var inline$foo1$1$x: int;
+  var inline$foo2$1$x: int;
+
+  anon0:
+    x := x + 1;
+    goto inline$foo3$0$Entry;
+
+  inline$foo3$0$Entry:
+    inline$foo3$0$x := x;
+    goto inline$foo3$0$anon0;
+
+  inline$foo3$0$anon0:
+    x := x + 1;
+    goto inline$foo1$0$Entry;
+
+  inline$foo1$0$Entry:
+    inline$foo1$0$x := x;
+    goto inline$foo1$0$anon0;
+
+  inline$foo1$0$anon0:
+    x := x + 1;
+    goto inline$foo2$0$Entry;
+
+  inline$foo2$0$Entry:
+    inline$foo2$0$x := x;
+    goto inline$foo2$0$anon0;
+
+  inline$foo2$0$anon0:
+    x := x + 1;
+    goto inline$foo3$1$Entry;
+
+  inline$foo3$1$Entry:
+    inline$foo3$1$x := x;
+    goto inline$foo3$1$anon0;
+
+  inline$foo3$1$anon0:
+    x := x + 1;
+    goto inline$foo1$1$Entry;
+
+  inline$foo1$1$Entry:
+    inline$foo1$1$x := x;
+    goto inline$foo1$1$anon0;
+
+  inline$foo1$1$anon0:
+    x := x + 1;
+    goto inline$foo2$1$Entry;
+
+  inline$foo2$1$Entry:
+    inline$foo2$1$x := x;
+    goto inline$foo2$1$anon0;
+
+  inline$foo2$1$anon0:
+    x := x + 1;
+    call foo3();
+    goto inline$foo2$1$Return;
+
+  inline$foo2$1$Return:
+    goto inline$foo1$1$anon0$1;
+
+  inline$foo1$1$anon0$1:
+    goto inline$foo1$1$Return;
+
+  inline$foo1$1$Return:
+    goto inline$foo3$1$anon0$1;
+
+  inline$foo3$1$anon0$1:
+    goto inline$foo3$1$Return;
+
+  inline$foo3$1$Return:
+    goto inline$foo2$0$anon0$1;
+
+  inline$foo2$0$anon0$1:
+    goto inline$foo2$0$Return;
+
+  inline$foo2$0$Return:
+    goto inline$foo1$0$anon0$1;
+
+  inline$foo1$0$anon0$1:
+    goto inline$foo1$0$Return;
+
+  inline$foo1$0$Return:
+    goto inline$foo3$0$anon0$1;
+
+  inline$foo3$0$anon0$1:
+    goto inline$foo3$0$Return;
+
+  inline$foo3$0$Return:
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo3();
+  modifies x;
+
+
+implementation {:inline 2} foo3()
+{
+  var inline$foo1$0$x: int;
+  var inline$foo2$0$x: int;
+  var inline$foo3$0$x: int;
+  var inline$foo1$1$x: int;
+  var inline$foo2$1$x: int;
+  var inline$foo3$1$x: int;
+
+  anon0:
+    x := x + 1;
+    goto inline$foo1$0$Entry;
+
+  inline$foo1$0$Entry:
+    inline$foo1$0$x := x;
+    goto inline$foo1$0$anon0;
+
+  inline$foo1$0$anon0:
+    x := x + 1;
+    goto inline$foo2$0$Entry;
+
+  inline$foo2$0$Entry:
+    inline$foo2$0$x := x;
+    goto inline$foo2$0$anon0;
+
+  inline$foo2$0$anon0:
+    x := x + 1;
+    goto inline$foo3$0$Entry;
+
+  inline$foo3$0$Entry:
+    inline$foo3$0$x := x;
+    goto inline$foo3$0$anon0;
+
+  inline$foo3$0$anon0:
+    x := x + 1;
+    goto inline$foo1$1$Entry;
+
+  inline$foo1$1$Entry:
+    inline$foo1$1$x := x;
+    goto inline$foo1$1$anon0;
+
+  inline$foo1$1$anon0:
+    x := x + 1;
+    goto inline$foo2$1$Entry;
+
+  inline$foo2$1$Entry:
+    inline$foo2$1$x := x;
+    goto inline$foo2$1$anon0;
+
+  inline$foo2$1$anon0:
+    x := x + 1;
+    goto inline$foo3$1$Entry;
+
+  inline$foo3$1$Entry:
+    inline$foo3$1$x := x;
+    goto inline$foo3$1$anon0;
+
+  inline$foo3$1$anon0:
+    x := x + 1;
+    call foo1();
+    goto inline$foo3$1$Return;
+
+  inline$foo3$1$Return:
+    goto inline$foo2$1$anon0$1;
+
+  inline$foo2$1$anon0$1:
+    goto inline$foo2$1$Return;
+
+  inline$foo2$1$Return:
+    goto inline$foo1$1$anon0$1;
+
+  inline$foo1$1$anon0$1:
+    goto inline$foo1$1$Return;
+
+  inline$foo1$1$Return:
+    goto inline$foo3$0$anon0$1;
+
+  inline$foo3$0$anon0$1:
+    goto inline$foo3$0$Return;
+
+  inline$foo3$0$Return:
+    goto inline$foo2$0$anon0$1;
+
+  inline$foo2$0$anon0$1:
+    goto inline$foo2$0$Return;
+
+  inline$foo2$0$Return:
+    goto inline$foo1$0$anon0$1;
+
+  inline$foo1$0$anon0$1:
+    goto inline$foo1$0$Return;
+
+  inline$foo1$0$Return:
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+after inlining procedure calls
+procedure bar();
+  modifies x;
+
+
+implementation bar()
+{
+  var inline$foo$0$x: int;
+  var inline$foo$1$x: int;
+  var inline$foo1$0$x: int;
+  var inline$foo2$0$x: int;
+  var inline$foo3$0$x: int;
+  var inline$foo1$1$x: int;
+  var inline$foo2$1$x: int;
+  var inline$foo3$1$x: int;
+
+  anon0:
+    goto inline$foo$0$Entry;
+
+  inline$foo$0$Entry:
+    inline$foo$0$x := x;
+    goto inline$foo$0$anon0;
+
+  inline$foo$0$anon0:
+    x := x + 1;
+    goto inline$foo$1$Entry;
+
+  inline$foo$1$Entry:
+    inline$foo$1$x := x;
+    goto inline$foo$1$anon0;
+
+  inline$foo$1$anon0:
+    x := x + 1;
+    call foo();
+    goto inline$foo$1$Return;
+
+  inline$foo$1$Return:
+    goto inline$foo$0$anon0$1;
+
+  inline$foo$0$anon0$1:
+    goto inline$foo$0$Return;
+
+  inline$foo$0$Return:
+    goto anon0$1;
+
+  anon0$1:
+    goto inline$foo1$0$Entry;
+
+  inline$foo1$0$Entry:
+    inline$foo1$0$x := x;
+    goto inline$foo1$0$anon0;
+
+  inline$foo1$0$anon0:
+    x := x + 1;
+    goto inline$foo2$0$Entry;
+
+  inline$foo2$0$Entry:
+    inline$foo2$0$x := x;
+    goto inline$foo2$0$anon0;
+
+  inline$foo2$0$anon0:
+    x := x + 1;
+    goto inline$foo3$0$Entry;
+
+  inline$foo3$0$Entry:
+    inline$foo3$0$x := x;
+    goto inline$foo3$0$anon0;
+
+  inline$foo3$0$anon0:
+    x := x + 1;
+    goto inline$foo1$1$Entry;
+
+  inline$foo1$1$Entry:
+    inline$foo1$1$x := x;
+    goto inline$foo1$1$anon0;
+
+  inline$foo1$1$anon0:
+    x := x + 1;
+    goto inline$foo2$1$Entry;
+
+  inline$foo2$1$Entry:
+    inline$foo2$1$x := x;
+    goto inline$foo2$1$anon0;
+
+  inline$foo2$1$anon0:
+    x := x + 1;
+    goto inline$foo3$1$Entry;
+
+  inline$foo3$1$Entry:
+    inline$foo3$1$x := x;
+    goto inline$foo3$1$anon0;
+
+  inline$foo3$1$anon0:
+    x := x + 1;
+    call foo1();
+    goto inline$foo3$1$Return;
+
+  inline$foo3$1$Return:
+    goto inline$foo2$1$anon0$1;
+
+  inline$foo2$1$anon0$1:
+    goto inline$foo2$1$Return;
+
+  inline$foo2$1$Return:
+    goto inline$foo1$1$anon0$1;
+
+  inline$foo1$1$anon0$1:
+    goto inline$foo1$1$Return;
+
+  inline$foo1$1$Return:
+    goto inline$foo3$0$anon0$1;
+
+  inline$foo3$0$anon0$1:
+    goto inline$foo3$0$Return;
+
+  inline$foo3$0$Return:
+    goto inline$foo2$0$anon0$1;
+
+  inline$foo2$0$anon0$1:
+    goto inline$foo2$0$Return;
+
+  inline$foo2$0$Return:
+    goto inline$foo1$0$anon0$1;
+
+  inline$foo1$0$anon0$1:
+    goto inline$foo1$0$Return;
+
+  inline$foo1$0$Return:
+    goto anon0$2;
+
+  anon0$2:
+    return;
+}
+
+
+
+Boogie program verifier finished with 5 verified, 0 errors