Boogie: Fixed a crash due to old expressions in lambda expressions that were not replaced after lambda expansion.

(reported by Florian Egli)

1 files changed, 16 insertions, 8 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index cb28cd7d..6752a2b7 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1201,14 +1201,7 @@ namespace VC {
       Contract.Assert(sortedNodes != null);

       #endregion

 

-      // Create substitution for old expressions

-      Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();

-      foreach (IdentifierExpr ie in modifies) {

-        Contract.Assert(ie != null);

-        if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))

-          oldFrameMap.Add(ie.Decl, ie);

-      }

-      Substitution oldFrameSubst = Substituter.SubstitutionFromHashtable(oldFrameMap);

+      Substitution oldFrameSubst = ComputeOldExpressionSubstitution(modifies);

 

       // Now we can process the nodes in an order so that we're guaranteed to have

       // processed all of a node's predecessors before we process the node.

@@ -1257,6 +1250,21 @@ namespace VC {
     }

 

     /// <summary>

+    /// Compute the substitution for old expressions.

+    /// </summary>

+    protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies)

+    {

+      Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();

+      foreach (IdentifierExpr ie in modifies)

+      {

+        Contract.Assert(ie != null);

+        if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))

+          oldFrameMap.Add(ie.Decl, ie);

+      }

+      return Substituter.SubstitutionFromHashtable(oldFrameMap);

+    }

+

+    /// <summary>

     /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc

     /// Meanwhile, record any information needed to later reconstruct a model view.

     /// </summary>