Enable marking if commands as {:allow_split} or not

Source/AbstractInterpretation/NativeLattice.cs

@@ -185,8 +185,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
       // We need to keep track of some information for each(some) block(s).  To do that efficiently,
       // we number the implementation's blocks sequentially, and then we can use arrays to store
       // the additional information.
-      var pre = new NativeLattice.Element[impl.Blocks
-        .Count]; // set to null if we never compute a join/widen at this block
+      var pre = new NativeLattice.Element[impl.Blocks.Count]; // set to null if we never compute a join/widen at this block
       var post = options.InstrumentInfer == CoreOptions.InstrumentationPlaces.Everywhere
         ? new NativeLattice.Element[impl.Blocks.Count]
         : null;
@@ -195,7 +194,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
       int n = 0;
       foreach (var block in impl.Blocks)
       {
-        block.aiId = n;
+        block.AiId = n;
         // Note:  The forward analysis below will store lattice elements in pre[n] if pre[n] is non-null.
         // Thus, the assignment "pre[n] = bottom;" below must be done under the following condition:
         //    n == 0 || block.widenBlock
@@ -219,7 +218,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
       {
         var workItem = workItems.Dequeue();
         var b = workItem.Item1;
-        var id = b.aiId;
+        var id = b.AiId;
         var e = workItem.Item2;
         if (pre[id] == null)
         {
@@ -230,7 +229,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
           // no change
           continue;
         }
-        else if (b.widenBlock && options.Ai.StepsBeforeWidening <= iterations[id])
+        else if (b.WidenBlock && options.Ai.StepsBeforeWidening <= iterations[id])
         {
           e = lattice.Widen(pre[id], e);
           pre[id] = e;
@@ -275,8 +274,8 @@ void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.
 
       foreach (var b in impl.Blocks)
       {
-        var element = pre[b.aiId];
-        if (element != null && (b.widenBlock || options.InstrumentInfer ==
+        var element = pre[b.AiId];
+        if (element != null && (b.WidenBlock || options.InstrumentInfer ==
           CoreOptions.InstrumentationPlaces.Everywhere))
         {
           List<Cmd> newCommands = new List<Cmd>();
@@ -294,9 +293,9 @@ void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.
 
           newCommands.Add(cmd);
           newCommands.AddRange(b.Cmds);
-          if (post != null && post[b.aiId] != null)
+          if (post != null && post[b.AiId] != null)
           {
-            inv = post[b.aiId].ToExpr(options);
+            inv = post[b.AiId].ToExpr(options);
             kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
             if (options.InstrumentWithAsserts)
             {

Source/AbstractInterpretation/Traverse.cs

@@ -54,7 +54,7 @@ static void Visit(Block b)
       {
         cce.BeginExpose(b);
         // we got here through a back-edge
-        b.widenBlock = true;
+        b.WidenBlock = true;
         cce.EndExpose();
       }
       else if (b.TraversingStatus == Block.VisitState.AlreadyVisited)
@@ -111,7 +111,7 @@ static void Visit(Block b)
     /// </summary>
     public static List<Block> ComputeLoopBodyFrom(Block block)
     {
-      Contract.Requires(block.widenBlock);
+      Contract.Requires(block.WidenBlock);
       Contract.Requires(block != null);
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
 

Source/Concurrency/LinearPermissionInstrumentation.cs

@@ -61,18 +61,18 @@ public List<Cmd> DisjointnessAndWellFormedAssumeCmds(Absy absy, bool addGlobals)
     public void AddDisjointnessAndWellFormedAssumptions(Implementation impl)
     {
       // calls and parallel calls
-      foreach (var b in impl.Blocks)
+      foreach (var block in impl.Blocks)
       {
         var newCmds = new List<Cmd>();
-        foreach (var cmd in b.Cmds)
+        foreach (var cmd in block.Cmds)
         {
           newCmds.Add(cmd);
           if (cmd is ParCallCmd)
           {
             newCmds.AddRange(DisjointnessAndWellFormedAssumeCmds(cmd, true));
           }
         }
-        b.Cmds = newCmds;
+        block.Cmds = newCmds;
       }
 
       // loop headers

Source/Concurrency/LinearTypeChecker.cs

@@ -852,14 +852,14 @@ void ProcessIfCmd(IfCmd ifCmd)
                   {
                     checkingContext.Error(ifCmd.tok, "access to linear store not allowed");
                   }
-                  stmtLists.Push(ifCmd.thn);
-                  if (ifCmd.elseIf != null)
+                  stmtLists.Push(ifCmd.Thn);
+                  if (ifCmd.ElseIf != null)
                   {
-                    ProcessIfCmd(ifCmd.elseIf);
+                    ProcessIfCmd(ifCmd.ElseIf);
                   }
-                  else if (ifCmd.elseBlock != null)
+                  else if (ifCmd.ElseBlock != null)
                   {
-                    stmtLists.Push(ifCmd.elseBlock);
+                    stmtLists.Push(ifCmd.ElseBlock);
                   }
                 }
                 ProcessIfCmd(ifCmd);

Source/Concurrency/YieldingProcInstrumentation.cs

@@ -482,9 +482,9 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
           var addEdge = false;
           foreach (var nextBlock in gotoCmd.LabelTargets)
           {
-            if (nextBlock.cmds.Count > 0)
+            if (nextBlock.Cmds.Count > 0)
             {
-              var cmd = nextBlock.cmds[0];
+              var cmd = nextBlock.Cmds[0];
               if (cmd is ParCallCmd parCallCmd)
               {
                 foreach (var callCmd in parCallCmd.CallCmds)
@@ -530,9 +530,9 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
       // desugar ParCallCmd 
       foreach (Block b in impl.Blocks)
       {
-        if (b.cmds.Count > 0)
+        if (b.Cmds.Count > 0)
         {
-          var cmd = b.cmds[0];
+          var cmd = b.Cmds[0];
           if (cmd is ParCallCmd)
           {
             DesugarParCallCmdInBlock(b, blocksInYieldingLoops.Contains(b));
@@ -578,27 +578,27 @@ private void SplitBlocks(Implementation impl)
       {
         var currTransferCmd = b.TransferCmd;
         int labelCount = 0;
-        int lastSplitIndex = b.cmds.Count;
-        for (int i = b.cmds.Count - 1; i >= 0; i--)
+        int lastSplitIndex = b.Cmds.Count;
+        for (int i = b.Cmds.Count - 1; i >= 0; i--)
         {
           var split = false;
-          var cmd = b.cmds[i];
+          var cmd = b.Cmds[i];
           if (cmd is ParCallCmd)
           {
             split = true;
           }
 
           if (split)
           {
-            var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.cmds.GetRange(i, lastSplitIndex - i),
+            var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.Cmds.GetRange(i, lastSplitIndex - i),
               currTransferCmd);
             newBlocks.Add(newBlock);
             currTransferCmd = new GotoCmd(b.tok, new List<Block> {newBlock});
             lastSplitIndex = i;
           }
         }
 
-        b.cmds = b.cmds.GetRange(0, lastSplitIndex);
+        b.Cmds = b.Cmds.GetRange(0, lastSplitIndex);
         b.TransferCmd = currTransferCmd;
       }
 
@@ -714,8 +714,8 @@ private void DesugarParCallCmdInBlock(Block block, bool isBlockInYieldingLoop)
       newCmds.AddRange(CreateUpdatesToOldGlobalVars());
       newCmds.AddRange(refinementInstrumentation.CreateUpdatesToOldOutputVars());
       newCmds.AddRange(CreateUpdatesToPermissionCollector(parCallCmd));
-      newCmds.AddRange(block.cmds.GetRange(1, block.cmds.Count - 1));
-      block.cmds = newCmds;
+      newCmds.AddRange(block.Cmds.GetRange(1, block.Cmds.Count - 1));
+      block.Cmds = newCmds;
     }
 
     private Formal ParCallDesugarFormal(Variable v, int count, bool incoming)

Source/Core/AST/Absy.cs

@@ -2490,7 +2490,7 @@ public String ErrorMessage
 
     public bool CanAlwaysAssume ()
     {
-      return Free && this.Attributes.FindBoolAttribute("always_assume");
+      return Free && Attributes.FindBoolAttribute("always_assume");
     }
 
     public Ensures(IToken token, bool free, Expr condition, string comment, QKeyValue kv)

Source/Core/AST/Commands/AbsyCmd.cs

@@ -3,12 +3,9 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Diagnostics.Contracts;
-using Set = Microsoft.Boogie.GSet<object>;
 
 namespace Microsoft.Boogie
 {
-  //---------------------------------------------------------------------
-  // Commands
   [ContractClassFor(typeof(Cmd))]
   public abstract class CmdContracts : Cmd
   {
@@ -2088,8 +2085,7 @@ public override Absy StdDispatch(StandardVisitor visitor)
 
   public class ReturnExprCmd : ReturnCmd
   {
-    public Expr /*!*/
-      Expr;
+    public Expr /*!*/ Expr;
 
     [ContractInvariantMethod]
     void ObjectInvariant()
@@ -2214,21 +2210,4 @@ public override Absy StdDispatch(StandardVisitor visitor)
       return visitor.VisitHavocCmd(this);
     }
   }
-
-  //---------------------------------------------------------------------
-  // Transfer commands
-
-  [ContractClassFor(typeof(TransferCmd))]
-  public abstract class TransferCmdContracts : TransferCmd
-  {
-    public TransferCmdContracts() : base(null)
-    {
-    }
-
-    public override void Emit(TokenTextWriter stream, int level)
-    {
-      Contract.Requires(stream != null);
-      throw new NotImplementedException();
-    }
-  }
 }

Source/Core/AST/Commands/CallCmd.cs

@@ -899,7 +899,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
         Contract.Assert(a != null);
         // These probably won't have IDs, but copy if they do.
         if (callId is not null) {
-          (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req,
+          a.CopyIdWithModificationsFrom(tok, req,
             id => new TrackedCallRequiresAssumed(callId, id));
         }
 

Source/Core/AST/Expression/AbsyExpr.cs

@@ -3890,7 +3890,7 @@ public class CodeExpr : Expr
     public List<Variable> /*!*/
       LocVars;
 
-    [Rep] public List<Block /*!*/> /*!*/ Blocks;
+    [Rep] public IList<Block /*!*/> /*!*/ Blocks;
 
     [ContractInvariantMethod]
     void ObjectInvariant()