Prevent creating return commands with empty tokens when copying blocks

Source/Core/AST/Block.cs

@@ -128,8 +128,8 @@ public bool IsLive(Variable v)
     return liveVarsBefore.Contains(v);
   }
 
-  public Block()
-    : this(Token.NoToken, "", new List<Cmd>(), new ReturnCmd(Token.NoToken))
+  public Block(IToken tok)
+    : this(tok, "", new List<Cmd>(), new ReturnCmd(tok))
   {
   }
 

Source/Core/VariableDependenceAnalyser.cs

@@ -523,7 +523,7 @@ private Dictionary<Block, HashSet<Block>> ComputeGlobalControlDependences()
       foreach (var Impl in prog.NonInlinedImplementations())
       {
         Graph<Block> blockGraph = prog.ProcessLoops(options, Impl);
-        LocalCtrlDeps[Impl] = blockGraph.ControlDependence();
+        LocalCtrlDeps[Impl] = blockGraph.ControlDependence(new Block(prog.tok));
         foreach (var KeyValue in LocalCtrlDeps[Impl])
         {
           GlobalCtrlDep.Add(KeyValue.Key, KeyValue.Value);

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.2.3</Version>
+    <Version>3.2.4</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/Graph/Graph.cs

@@ -1211,7 +1211,7 @@ public static IEnumerable<object> FindReachableNodesInGraphWithMergeNodes(
 
     public static Graph<Node> Dual<Node>(this Graph<Node> g, Node dummySource)
     {
-      var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList();
+      var exits = g.Nodes.Where(n => !g.Successors(n).Any()).ToList();
       Node source;
       if (exits.Count == 0)
       {
@@ -1373,9 +1373,9 @@ public static List<Tuple<Node, bool>> LoopyTopSort<Node>(this Graph<Node> g)
 
     // Algorithm from Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren,
     // "The Program Dependence Graph and Its Use in Optimization"
-    public static Dictionary<Node, HashSet<Node>> ControlDependence<Node>(this Graph<Node> g) where Node : class, new()
+    public static Dictionary<Node, HashSet<Node>> ControlDependence<Node>(this Graph<Node> g, Node dummySource) where Node : class
     {
-      Graph<Node> dual = g.Dual(new Node());
+      Graph<Node> dual = g.Dual(dummySource);
       DomRelation<Node> pdom = dual.DominatorMap;
 
       var result = new Dictionary<Node, HashSet<Node>>();

Source/VCGeneration/LoopExtractor.cs

@@ -311,8 +311,10 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G
             continue;
           }
 
-          Block newBlock = new Block();
-          newBlock.Label = block.Label;
+          Block newBlock = new Block(block.tok)
+          {
+            Label = block.Label
+          };
           if (headRecursion && block == header)
           {
             CallCmd callCmd = (CallCmd) (loopHeaderToCallCmd2[header]).Clone();
@@ -330,10 +332,13 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G
           blockMap[block] = newBlock;
           if (newBlocksCreated.ContainsKey(block))
           {
-            Block newBlock2 = new Block();
-            newBlock2.Label = newBlocksCreated[block].Label;
-            newBlock2.Cmds = Substituter.Apply(subst, newBlocksCreated[block].Cmds);
-            blockMap[newBlocksCreated[block]] = newBlock2;
+            var original = newBlocksCreated[block];
+            var newBlock2 = new Block(original.tok)
+            {
+              Label = original.Label,
+              Cmds = Substituter.Apply(subst, original.Cmds)
+            };
+            blockMap[original] = newBlock2;
           }
 
           //for detLoopExtract, need the immediate successors even outside the loop
@@ -349,15 +354,16 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G
               if (g.Nodes.Contains(bl) && //newly created blocks are not present in NaturalLoop(header, xx, g)
                   !loopNodes.Contains(bl))
               {
-                Block auxNewBlock = new Block();
-                auxNewBlock.Label = bl.Label;
-                //these blocks may have read/write locals that are not present in naturalLoops
-                //we need to capture these variables
-                auxNewBlock.Cmds = Substituter.Apply(subst, bl.Cmds);
+                var auxNewBlock = new Block(bl.tok)
+                {
+                  Label = bl.Label,
+                  //these blocks may have read/write locals that are not present in naturalLoops
+                  //we need to capture these variables
+                  Cmds = Substituter.Apply(subst, bl.Cmds)
+                };
                 //add restoration code for such blocks
-                if (loopHeaderToAssignCmd.ContainsKey(header))
+                if (loopHeaderToAssignCmd.TryGetValue(header, out var assignCmd))
                 {
-                  AssignCmd assignCmd = loopHeaderToAssignCmd[header];
                   auxNewBlock.Cmds.Add(assignCmd);
                 }
 

Source/VCGeneration/ManualSplitFinder.cs

@@ -96,10 +96,11 @@ private static List<Block> DoPreAssignedManualSplit(VCGenOptions options, List<B
     //var duplicator = new Duplicator();
     var oldToNewBlockMap = new Dictionary<Block, Block>(blocks.Count); // Maps original blocks to their new copies in newBlocks
     foreach (var currentBlock in blocks) {
-      var newBlock = new Block();
-      newBlock.Label = currentBlock.Label;
-      newBlock.tok = currentBlock.tok;
-
+      var newBlock = new Block(currentBlock.tok)
+      {
+        Label = currentBlock.Label
+      };
+
       oldToNewBlockMap[currentBlock] = newBlock;
       newBlocks.Add(newBlock);
       if (currentBlock == containingBlock) {