From 9764fbc35fa11d27c1dabe1d55a08397aa041e04 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jan 2024 14:06:32 +0100 Subject: [PATCH] Refactoring --- Source/ExecutionEngine/ExecutionEngine.cs | 4 +--- Source/VCGeneration/ManualSplitFinder.cs | 9 ++++++--- Source/VCGeneration/SplitAndVerifyWorker.cs | 7 ++----- 3 files changed, 9 insertions(+), 11 deletions(-) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 317c18190..97bf3ff5f 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -724,9 +724,7 @@ public IReadOnlyList 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 index b3ec8021b..f05e5cdfe 100644 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -8,17 +8,20 @@ namespace VCGeneration; public static class ManualSplitFinder { - public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par, bool splitOnEveryAssert) + public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) { List 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 FindManualSplits(Split initialSplit, bool splitOnEveryAssert) + public static List FindManualSplits(Split initialSplit) { Contract.Requires(initialSplit.Implementation != null); Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); + var splitOnEveryAssert = initialSplit.Options.VcsSplitOnEveryAssert; + initialSplit.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); + var splitPoints = new Dictionary(); foreach (var block in initialSplit.Blocks) { diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index 29d7da937..3ea80a454 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -21,9 +21,8 @@ public class SplitAndVerifyWorker private readonly int maxKeepGoingSplits; public List 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);