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/houdini/Answer      | 10 ++++++++++
 Test/houdini/runtest.bat |  6 ++++++
 Test/houdini/test7.bpl   | 15 +++++++++++++++
 Test/houdini/test8.bpl   | 21 +++++++++++++++++++++
 4 files changed, 52 insertions(+)
 create mode 100644 Test/houdini/test7.bpl
 create mode 100644 Test/houdini/test8.bpl

(limited to 'Test/houdini')

diff --git a/Test/houdini/Answer b/Test/houdini/Answer
index 94ae7f04..60ae7d80 100644
--- a/Test/houdini/Answer
+++ b/Test/houdini/Answer
@@ -99,3 +99,13 @@ b6 = False
 b7 = False
 
 Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- test7.bpl --------------------
+Assignment computed by Houdini:
+
+Boogie program verifier finished with 2 verified, 0 errors
+.
+-------------------- test8.bpl --------------------
+Assignment computed by Houdini:
+
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat
index d0e53b08..40f8cea0 100644
--- a/Test/houdini/runtest.bat
+++ b/Test/houdini/runtest.bat
@@ -8,3 +8,9 @@ for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bp
   echo -------------------- %%f --------------------
   %BGEXE% %* /nologo /noinfer /contractInfer %%f
 )
+
+for %%f in (test7.bpl test8.bpl) do (
+  echo .
+  echo -------------------- %%f --------------------
+  %BGEXE% %* /nologo /noinfer /contractInfer /inline:spec /inlineDepth:1 %%f
+)
diff --git a/Test/houdini/test7.bpl b/Test/houdini/test7.bpl
new file mode 100644
index 00000000..b5c6a4c6
--- /dev/null
+++ b/Test/houdini/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/houdini/test8.bpl b/Test/houdini/test8.bpl
new file mode 100644
index 00000000..12eab481
--- /dev/null
+++ b/Test/houdini/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