fixed bug in the inlineDepth option for houdini

small clean up in the inlining implementation

4 files changed, 0 insertions, 232 deletions

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