Fixed bug in inlining (procedure *definitions* had been traversed by StandardVisitor while visiting commands).

This solves Issue #6266.

3 files changed, 24 insertions, 3 deletions

diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc
index 1e0ceb8f..192ed7a4 100644
--- a/Source/Core/StandardVisitor.ssc
+++ b/Source/Core/StandardVisitor.ssc
@@ -148,7 +148,6 @@ namespace Microsoft.Boogie
       for (int i = 0; i < node.Outs.Count; ++i)

         if (node.Outs[i] != null)

           node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr((!)node.Outs[i]);

-      node.Proc = this.VisitProcedure((!)node.Proc);

       return node; 

     }

     public virtual Cmd! VisitCallForallCmd(CallForallCmd! node)

@@ -349,7 +348,6 @@ namespace Microsoft.Boogie
     public virtual Expr! VisitNAryExpr(NAryExpr! node)

     {

       node.Args = this.VisitExprSeq(node.Args);

-//      if (node.Type != null) { node.Type = this.VisitType(node.Type); } // BUGBUG? Do this even though it 

       return node; 

     }

     public virtual Expr! VisitOldExpr(OldExpr! node)

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();

+}