Refactoring

boogie-org · Jan 26, 2024 · 9764fbc · 9764fbc
1 parent d6446ab
commit 9764fbc
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 11 deletions.
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -724,9 +724,7 @@ public IReadOnlyList<IVerificationTask> GetVerificationTasks(Program program) {
           out var gotoCmdOrigins,
           out var modelViewInfo);
 
-        var splitOnEveryAssert = Options.VcsSplitOnEveryAssert;
-        run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert);
-        var splits = ManualSplitFinder.FocusAndSplit(Options, run, gotoCmdOrigins, vcGenerator, splitOnEveryAssert);
+        var splits = ManualSplitFinder.FocusAndSplit(Options, run, gotoCmdOrigins, vcGenerator);
         return splits.Select(split => new VerificationTask(this, processedProgram, split, modelViewInfo));
       }).ToList();
     }

diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs
@@ -8,17 +8,20 @@ namespace VCGeneration;
 
 public static class ManualSplitFinder
 {
-  public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerificationConditionGenerator par, bool splitOnEveryAssert)
+  public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerificationConditionGenerator par)
   {
     List<Split> focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par);
-    return focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList();
+    return focussedImpl.Select(FindManualSplits).SelectMany(x => x).ToList();
   }
 
-  public static List<Split /*!*/> FindManualSplits(Split initialSplit, bool splitOnEveryAssert)
+  public static List<Split /*!*/> FindManualSplits(Split initialSplit)
   {
     Contract.Requires(initialSplit.Implementation != null);
     Contract.Ensures(Contract.Result<List<Split>>() == null || cce.NonNullElements(Contract.Result<List<Split>>()));
 
+    var splitOnEveryAssert = initialSplit.Options.VcsSplitOnEveryAssert;
+    initialSplit.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert);
+
     var splitPoints = new Dictionary<Block, int>();
     foreach (var block in initialSplit.Blocks)
     {

diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs
@@ -21,9 +21,8 @@ public class SplitAndVerifyWorker
   private readonly int maxKeepGoingSplits;
   public List<Split> ManualSplits { get; }
   private double maxVcCost;
-  private readonly bool splitOnEveryAssert;
 
-  private bool DoSplitting => ManualSplits.Count > 1 || KeepGoing || splitOnEveryAssert;
+  private bool DoSplitting => ManualSplits.Count > 1 || KeepGoing;
   private bool TrackingProgress => DoSplitting && (callback.OnProgress != null || options.Trace); 
   private bool KeepGoing => maxKeepGoingSplits > 1;
 
@@ -58,11 +57,9 @@ public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator
       maxVcCost = tmpMaxVcCost;
     }
 
-    splitOnEveryAssert = options.VcsSplitOnEveryAssert;
-    Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert);
 
     ResetPredecessors(Implementation.Blocks);
-    ManualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator, splitOnEveryAssert);
+    ManualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator);
 
     if (ManualSplits.Count == 1 && maxSplits > 1) {
       ManualSplits = Split.DoSplit(ManualSplits[0], maxVcCost, maxSplits);