From 8a3d35545386c74864db0662faa5c1d68cd71f01 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 19 Nov 2009 18:51:13 +0000
Subject: Fixed bug in inlining (procedure *definitions* had been traversed by
 StandardVisitor while visiting commands). This solves Issue #6266.

---
 Test/inline/Answer    |  2 +-
 Test/inline/test5.bpl | 23 +++++++++++++++++++++++
 2 files changed, 24 insertions(+), 1 deletion(-)

(limited to 'Test/inline')

diff --git a/Test/inline/Answer b/Test/inline/Answer
index 8f2c34e4..854ac558 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -893,7 +893,7 @@ Execution trace:
     test5.bpl(25,23): inline$P$1$Return
     test5.bpl(34,10): anon0$2
 
-Boogie program verifier finished with 3 verified, 1 error
+Boogie program verifier finished with 4 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 629cb04c..6460232c 100644
--- a/Test/inline/test5.bpl
+++ b/Test/inline/test5.bpl
@@ -54,3 +54,26 @@ procedure mainC()
   call P(1);
   assert Mem[1] == 1;  // good
 }
+
+// -------------------------------------------------
+
+type ref;
+var xyz: ref;
+
+procedure xyzA();
+  modifies xyz;
+  ensures old(xyz) == xyz;
+
+procedure {:inline 1} xyzB()
+  modifies xyz;
+{
+  call xyzA();
+}
+
+procedure xyzMain()
+  modifies xyz;
+{
+  call xyzA();
+  assert old(xyz) == xyz;
+  call xyzB();
+}
-- 
cgit v1.2.3