Fixes

boogie-org · Oct 16, 2024 · ff278bf · ff278bf
1 parent 1d31906
commit ff278bf
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 5 deletions.
diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs
@@ -99,7 +99,7 @@ private static bool ContainsAssert(Block b)
   public static void DeleteStraightLineBlocksWithoutCommands(IList<Block> blocks) {
     var toVisit = new HashSet<Block>(blocks);
     var removed = new HashSet<Block>();
-    while(toVisit.Count > 0) {
+    while(toVisit.Count > 0 && blocks.Count > 1) {
       var block = toVisit.First();
       toVisit.Remove(block);
       if (removed.Contains(block)) {
@@ -121,6 +121,7 @@ public static void DeleteStraightLineBlocksWithoutCommands(IList<Block> blocks)
         var successor = gotoCmd2.LabelTargets.FirstOrDefault();
         if (successor != null && !successor.tok.IsValid && block.tok.IsValid) {
           successor.tok = block.tok;
+          successor.Label = block.Label; 
         }
       }
 
@@ -129,6 +130,7 @@ public static void DeleteStraightLineBlocksWithoutCommands(IList<Block> blocks)
         var predecessor = block.Predecessors.First();
         if (!predecessor.tok.IsValid && block.tok.IsValid) {
           predecessor.tok = block.tok;
+          predecessor.Label = block.Label; // TODO should update targetLabels
         }
       }
 

diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs
@@ -25,9 +25,9 @@ public static IEnumerable<ManualSplit> GetParts(VCGenOptions options, Implementa
         return isolatedAssertions.Concat(splitParts).ToList();
       });
     });
-    return result;
-    // var nonEmptyResults = result.Where(s => s.Asserts.Any()).ToList();
-    // return nonEmptyResults.Any() ? nonEmptyResults : focussedParts;
+    // return result;
+    var nonEmptyResults = result.Where(s => s.Asserts.Any()).ToList();
+    return nonEmptyResults.Any() ? nonEmptyResults : focussedParts;
   }
 }
 

diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs
@@ -764,7 +764,8 @@ public void PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo)
       {
         #region Get rid of empty blocks
         {
-          RemoveEmptyBlocks(impl.Blocks.ToList());
+          // RemoveEmptyBlocks(impl.Blocks.ToList());
+          var copy = impl.Blocks.ToList();
           BlockTransformations.DeleteStraightLineBlocksWithoutCommands(impl.Blocks);
           impl.PruneUnreachableBlocks(Options);
         }