Merge

2 files changed, 61 insertions, 16 deletions

diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
index 987574be..dcdb087f 100644
--- a/Source/VCGeneration/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -77,10 +77,14 @@ public class BlockPredicator {
         // the first statement in the block.
         var assign = cmdSeq.Last();
         cmdSeq.Truncate(cmdSeq.Length-1);
-        cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(pExpr, aCmd.Expr)));
+        aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr);
+        cmdSeq.Add(aCmd);
+        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));
         cmdSeq.Add(assign);
       } else {
-        cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+        aCmd.Expr = Expr.Imp(p, aCmd.Expr);
+        cmdSeq.Add(aCmd);
+        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr)));
       }
     } else if (cmd is AssumeCmd) {
       var aCmd = (AssumeCmd)cmd;
@@ -114,15 +118,20 @@ public class BlockPredicator {
       var cCmd = (CallCmd)cmd;
       cCmd.Ins.Insert(0, p);
       cmdSeq.Add(cCmd);
-    } else if (cmd is StateCmd) {
-      var sCmd = (StateCmd)cmd;
-      var newCmdSeq = new CmdSeq();
-      foreach (Cmd c in sCmd.Cmds)
-        PredicateCmd(newCmdSeq, c);
-      sCmd.Cmds = newCmdSeq;
-      cmdSeq.Add(sCmd);
-    } else {
-      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+    }
+    else if (cmd is CommentCmd) {
+      // skip

+    }

+    else if (cmd is StateCmd) {

+      var sCmd = (StateCmd)cmd;

+      var newCmdSeq = new CmdSeq();

+      foreach (Cmd c in sCmd.Cmds)

+        PredicateCmd(newCmdSeq, c);

+      sCmd.Cmds = newCmdSeq;

+      cmdSeq.Add(sCmd);

+    }

+    else {

+      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());

     }
   }
 
@@ -298,13 +307,23 @@ public class BlockPredicator {
         dwf.InParams = new VariableSeq(
           (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
             .ToArray());
-      }
-      var impl = decl as Implementation;
-      if (impl != null)
-        new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();
+      }

+      try {

+        var impl = decl as Implementation;

+        if (impl != null)

+          new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();

+      }

+      catch (Program.IrreducibleLoopException) { }
     }
   }
 
+  public static void Predicate(Program p, Implementation impl) {

+    try {

+      new BlockPredicator(p, impl, false, false).PredicateImplementation();

+    }

+    catch (Program.IrreducibleLoopException) { }
+  }
+
 }
 
 }
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 373b685a..1c3fa979 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1968,6 +1968,26 @@ namespace VC {
       #endregion

     }

 

+    public void DesugarCalls(Implementation impl) {

+      foreach (Block block in impl.Blocks) {

+        CmdSeq newCmds = new CmdSeq();

+        foreach (Cmd cmd in block.Cmds) {

+          SugaredCmd sugaredCmd = cmd as SugaredCmd;

+          if (sugaredCmd != null) {

+            StateCmd stateCmd = sugaredCmd.Desugaring as StateCmd;

+            foreach (Variable v in stateCmd.Locals) {

+              impl.LocVars.Add(v);

+            }

+            newCmds.AddRange(stateCmd.Cmds);

+          }

+          else {

+            newCmds.Add(cmd);

+          }

+        }

+        block.Cmds = newCmds;

+      }

+    }

+

     public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)

     {

       Contract.Requires(impl != null);

@@ -2035,7 +2055,13 @@ namespace VC {
         EmitImpl(impl, true);

       }

       #endregion

-    

+

+      if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining == 0) {

+        DesugarCalls(impl);

+        BlockPredicator.Predicate(program, impl);

+        impl.ComputePredecessorsForBlocks();

+      }

+

       if (CommandLineOptions.Clo.LiveVariableAnalysis > 0) {

         Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

       }