From df1cd695daffb01a590a7310dbee1b6594de2ecd Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Wed, 23 Nov 2011 11:26:34 -0800
Subject: fixed bug in the inlineDepth option for houdini small clean up in the
 inlining implementation

---
 Test/inline/Answer      | 191 ------------------------------------------------
 Test/inline/runtest.bat |   5 --
 Test/inline/test7.bpl   |  15 ----
 Test/inline/test8.bpl   |  21 ------
 4 files changed, 232 deletions(-)
 delete mode 100644 Test/inline/test7.bpl
 delete mode 100644 Test/inline/test8.bpl

(limited to 'Test/inline')

diff --git a/Test/inline/Answer b/Test/inline/Answer
index d7e7edbe..6f63f1e3 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1439,197 +1439,6 @@ implementation bar()
 
 
 Boogie program verifier finished with 5 verified, 0 errors
--------------------- test7.bpl --------------------
-
-var g: int;
-
-procedure main();
-  modifies g;
-
-
-
-implementation main()
-{
-
-  anon0:
-    g := 0;
-    call foo();
-    assert g == 1;
-    return;
-}
-
-
-
-procedure foo();
-  modifies g;
-
-
-
-implementation foo()
-{
-
-  anon0:
-    g := g + 1;
-    return;
-}
-
-
-after inlining procedure calls
-procedure main();
-  modifies g;
-
-
-implementation main()
-{
-  var inline$foo$0$g: int;
-
-  anon0:
-    g := 0;
-    goto inline$foo$0$Entry;
-
-  inline$foo$0$Entry:
-    inline$foo$0$g := g;
-    goto inline$foo$0$anon0;
-
-  inline$foo$0$anon0:
-    g := g + 1;
-    goto inline$foo$0$Return;
-
-  inline$foo$0$Return:
-    goto anon0$1;
-
-  anon0$1:
-    assert g == 1;
-    return;
-}
-
-
-
-Boogie program verifier finished with 2 verified, 0 errors
--------------------- test8.bpl --------------------
-
-var g: int;
-
-procedure main();
-  modifies g;
-
-
-
-implementation main()
-{
-
-  anon0:
-    g := 0;
-    call foo();
-    assert g == 1;
-    return;
-}
-
-
-
-procedure {:inline 1} foo();
-  modifies g;
-
-
-
-implementation {:inline 1} foo()
-{
-
-  anon0:
-    call bar();
-    return;
-}
-
-
-
-procedure bar();
-  modifies g;
-
-
-
-implementation bar()
-{
-
-  anon0:
-    g := g + 1;
-    return;
-}
-
-
-after inlining procedure calls
-procedure main();
-  modifies g;
-
-
-implementation main()
-{
-  var inline$foo$0$g: int;
-  var inline$bar$0$g: int;
-
-  anon0:
-    g := 0;
-    goto inline$foo$0$Entry;
-
-  inline$foo$0$Entry:
-    inline$foo$0$g := g;
-    goto inline$foo$0$anon0;
-
-  inline$foo$0$anon0:
-    goto inline$bar$0$Entry;
-
-  inline$bar$0$Entry:
-    inline$bar$0$g := g;
-    goto inline$bar$0$anon0;
-
-  inline$bar$0$anon0:
-    g := g + 1;
-    goto inline$bar$0$Return;
-
-  inline$bar$0$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:
-    assert g == 1;
-    return;
-}
-
-
-after inlining procedure calls
-procedure {:inline 1} foo();
-  modifies g;
-
-
-implementation {:inline 1} foo()
-{
-  var inline$bar$0$g: int;
-
-  anon0:
-    goto inline$bar$0$Entry;
-
-  inline$bar$0$Entry:
-    inline$bar$0$g := g;
-    goto inline$bar$0$anon0;
-
-  inline$bar$0$anon0:
-    g := g + 1;
-    goto inline$bar$0$Return;
-
-  inline$bar$0$Return:
-    goto anon0$1;
-
-  anon0$1:
-    return;
-}
-
-
-
-Boogie program verifier finished with 3 verified, 0 errors
 -------------------- test5.bpl --------------------
 test5.bpl(37,3): Error BP5001: This assertion might not hold.
 Execution trace:
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
index 3a8b0a9d..f56d55a0 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -13,11 +13,6 @@ for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl test6.bpl) do (
   %BGEXE% %* /inline:spec /print:- /env:0 /printInlined /noinfer %%f
 )
 
-for %%f in (test7.bpl test8.bpl) do (
-  echo -------------------- %%f --------------------
-  %BGEXE% %* /inline:spec /inlineDepth:1 /print:- /env:0 /printInlined /noinfer %%f
-)
-
 for %%f in (test5.bpl expansion3.bpl expansion4.bpl Elevator.bpl) do (
   echo -------------------- %%f --------------------
   %BGEXE% %* %%f
diff --git a/Test/inline/test7.bpl b/Test/inline/test7.bpl
deleted file mode 100644
index b5c6a4c6..00000000
--- a/Test/inline/test7.bpl
+++ /dev/null
@@ -1,15 +0,0 @@
-var g: int;
-
-procedure main() 
-modifies g;
-{
-  g := 0;
-  call foo();
-  assert g == 1;
-}
-
-procedure foo() 
-modifies g;
-{
-  g := g + 1;
-}
\ No newline at end of file
diff --git a/Test/inline/test8.bpl b/Test/inline/test8.bpl
deleted file mode 100644
index 12eab481..00000000
--- a/Test/inline/test8.bpl
+++ /dev/null
@@ -1,21 +0,0 @@
-var g: int;
-
-procedure main() 
-modifies g;
-{
-  g := 0;
-  call foo();
-  assert g == 1;
-}
-
-procedure {:inline 1} foo() 
-modifies g;
-{
-  call bar();
-}
-
-procedure bar()
-modifies g;
-{
-  g := g + 1;
-}
\ No newline at end of file
-- 
cgit v1.2.3