From 7552293514e40a6dcd9749d3668519d7d32049d5 Mon Sep 17 00:00:00 2001
From: Unknown <shuvendu@SHUVENDU-Z400.redmond.corp.microsoft.com>
Date: Fri, 1 Jun 2012 01:36:11 -0700
Subject: 1. Fix for free ensures in inlined procedures. Becomes a skip instead
 of an assume. 2. Fix for deterministic loop extraction, and a new regression.
 3. All regressions (including Dafny) except houdini pass, it is most likely
 related to the free ensures change.

---
 Source/Core/Absy.cs | 35 +++++++++++++++++++----------------
 1 file changed, 19 insertions(+), 16 deletions(-)

(limited to 'Source/Core/Absy.cs')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index d7fcca7a..148a739d 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -590,7 +590,25 @@ namespace Microsoft.Boogie {
                     if (!found) {
                         Block auxNewBlock = new Block();
                         auxNewBlock.Label = ((Block)bl).Label;
-                        auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)block).Cmds);
+                        auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds);
+                        //add restoration code for such blocks
+                        if (loopHeaderToAssignCmd.ContainsKey(header))
+                        {
+                            AssignCmd assignCmd = loopHeaderToAssignCmd[header];
+                            auxNewBlock.Cmds.Add(assignCmd);
+                        }
+                        List<AssignLhs> lhsg = new List<AssignLhs>();
+                        IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;
+                        foreach (IdentifierExpr gl in globalsMods)
+                            lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));
+                        List<Expr> rhsg = new List<Expr>();
+                        foreach (IdentifierExpr gl in globalsMods)
+                            rhsg.Add(new OldExpr(Token.NoToken, gl));
+                        if (lhsg.Count != 0)
+                        {
+                            AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg);
+                            auxNewBlock.Cmds.Add(globalAssignCmd);
+                        }
                         blockMap[(Block)bl] = auxNewBlock;
                     }
                 }
@@ -666,21 +684,6 @@ namespace Microsoft.Boogie {
             if (newTargets.Length == 0) {
                 if (!detLoopExtract)
                     newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
-                else {
-                    if (loopHeaderToAssignCmd.ContainsKey(header)) {
-                        AssignCmd assignCmd = loopHeaderToAssignCmd[header];
-                        newBlock.Cmds.Add(assignCmd);
-                    }
-                    List<AssignLhs> lhsg = new List<AssignLhs>();
-                    IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;
-                    foreach (IdentifierExpr gl in globalsMods)
-                        lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));
-                    List<Expr> rhsg = new List<Expr>();
-                    foreach (IdentifierExpr gl in globalsMods)
-                        rhsg.Add(new OldExpr(Token.NoToken, gl));
-                    AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg);
-                    newBlock.Cmds.Add(globalAssignCmd);
-                }
                 newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
             } else {
               newBlock.TransferCmd = new GotoCmd(Token.NoToken, newLabels, newTargets);
-- 
cgit v1.2.3