From 163fc931061c2d3065ec7a0acba817357295c3d2 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Sun, 13 Nov 2011 17:25:28 -0800
Subject: added the option /inlineDepth:n. This option defaults to -1. If the
 user provides a non-negative number then that number is used to inline
 procedures not annotated by {:inline n} attribute.

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

(limited to 'Test/inline')

diff --git a/Test/inline/Answer b/Test/inline/Answer
index ae632f79..2c29ab0b 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1439,6 +1439,197 @@ 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 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 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 f56d55a0..3a8b0a9d 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -13,6 +13,11 @@ 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
new file mode 100644
index 00000000..b5c6a4c6
--- /dev/null
+++ b/Test/inline/test7.bpl
@@ -0,0 +1,15 @@
+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
new file mode 100644
index 00000000..12eab481
--- /dev/null
+++ b/Test/inline/test8.bpl
@@ -0,0 +1,21 @@
+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