From 2e2622a8746e85b8b704ec70adfd35d730e25c19 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Wed, 14 Oct 2009 00:48:23 +0000
Subject: Fixed bugs in inlining, and added a test case. This solves issue
 5742, as reported in the MSR Boogie Issue Tracker on Codeplex.

---
 Test/inline/Answer    | 15 +++++++++++++--
 Test/inline/test5.bpl | 36 ++++++++++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+), 2 deletions(-)

(limited to 'Test/inline')

diff --git a/Test/inline/Answer b/Test/inline/Answer
index 62d9b677..43ec6740 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -881,8 +881,19 @@ Execution trace:
 
 Boogie program verifier finished with 0 verified, 4 errors
 -------------------- test5.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
+test5.bpl(37,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    test5.bpl(34,10): anon0
+    test5.bpl(25,23): inline$P$0$Entry
+    test5.bpl(28,10): inline$P$0$anon0
+    test5.bpl(25,23): inline$P$0$Return
+    test5.bpl(34,10): anon0$1
+    test5.bpl(25,23): inline$P$1$Entry
+    test5.bpl(28,10): inline$P$1$anon0
+    test5.bpl(25,23): inline$P$1$Return
+    test5.bpl(34,10): anon0$2
+
+Boogie program verifier finished with 3 verified, 1 error
 -------------------- test6.bpl --------------------
 test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo
 test6.bpl(15,22): Error: the inlined procedure is recursive, call stack: foo2 -> foo3 -> foo1 -> foo2
diff --git a/Test/inline/test5.bpl b/Test/inline/test5.bpl
index 0132f60a..629cb04c 100644
--- a/Test/inline/test5.bpl
+++ b/Test/inline/test5.bpl
@@ -18,3 +18,39 @@ procedure  bar()
   assert x == 5;
 }
 
+// -------------------------------------------------
+
+var Mem : [int]int;
+
+procedure {:inline 1} P(x:int)
+  modifies Mem;
+{
+  Mem[x] := 1;
+}
+
+procedure mainA()
+  modifies Mem;
+{
+  Mem[1] := 0;
+  call P(0);
+  call P(1);
+  assert Mem[1] == 0;  // error
+}
+
+procedure mainB()
+  modifies Mem;
+{
+  Mem[1] := 0;
+  call P(0);
+  call P(1);
+  assert Mem[1] == 1;  // good
+}
+
+procedure mainC()
+  modifies Mem;
+{
+  Mem[1] := 0;
+  call P(0);
+  call P(1);
+  assert Mem[1] == 1;  // good
+}
-- 
cgit v1.2.3