From e426c84d47fde936eefc5e44790b5a652dd0a5b7 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sun, 13 Oct 2024 23:26:43 +0200 Subject: [PATCH 1/5] try filtering the splits --- Source/VCGeneration/Splits/ManualSplitFinder.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs index 4b553b055..1d260a917 100644 --- a/Source/VCGeneration/Splits/ManualSplitFinder.cs +++ b/Source/VCGeneration/Splits/ManualSplitFinder.cs @@ -21,7 +21,8 @@ public static IEnumerable GetParts(VCGenOptions options, Implementa IsolateAttributeOnAssertsHandler.GetParts(options, withoutIsolatedJumps, createPart); var splitParts = SplitAttributeHandler.GetParts(withoutIsolatedAssertions); - return isolatedJumps.Concat(isolatedAssertions).Concat(splitParts); + var splits = isolatedJumps.Concat(isolatedAssertions).Concat(splitParts).Where(s => s.Asserts.Any()).ToList(); + return splits.ToList().Any() ? splits.ToList() : new List { focussedPart }; }); return result; } From f303d01b2417b28485798c9530895c6763743ff5 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sun, 13 Oct 2024 23:34:50 +0200 Subject: [PATCH 2/5] revert unit test --- Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs index 2500faf71..85d1f41a1 100644 --- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs @@ -100,7 +100,7 @@ procedure Procedure(y: int) // The implicit return at the end gets a separate VC. // first split is empty. Maybe it can be optimized away - Assert.AreEqual(5, tasks.Count); + Assert.AreEqual(4, tasks.Count); var outcomes = new List { SolverOutcome.Invalid, SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid }; for (var index = 0; index < outcomes.Count; index++) From ddf8498f4bd30ad1e34972f27d055a1fc223923a Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sun, 13 Oct 2024 23:45:47 +0200 Subject: [PATCH 3/5] revert more tests --- Test/commandline/SplitOnEveryAssert.bpl | 24 ++++++++++++------------ Test/test0/SplitOnEveryAssert.bpl | 22 +++++++++++----------- 2 files changed, 23 insertions(+), 23 deletions(-) diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl index f65fd1203..19b275b60 100644 --- a/Test/commandline/SplitOnEveryAssert.bpl +++ b/Test/commandline/SplitOnEveryAssert.bpl @@ -3,18 +3,18 @@ // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: Verifying Ex ... -// CHECK: checking split 1/12 .* -// CHECK: checking split 2/12 .* -// CHECK: checking split 3/12 .* -// CHECK: checking split 4/12 .* -// CHECK: --> split #4 done, \[.* s\] Invalid -// CHECK: checking split 5/12 .* -// CHECK: checking split 6/12 .* -// CHECK: checking split 7/12 .* -// CHECK: checking split 8/12 .* -// CHECK: checking split 9/12 .* -// CHECK: checking split 10/12 .* -// CHECK: checking split 11/12 .* +// CHECK: checking split 1/11 .* +// CHECK: checking split 2/11 .* +// CHECK: checking split 3/11 .* +// CHECK: checking split 4/11 .* +// CHECK: --> split #3 done, \[.* s\] Invalid +// CHECK: checking split 5/11 .* +// CHECK: checking split 6/11 .* +// CHECK: checking split 7/11 .* +// CHECK: checking split 8/11 .* +// CHECK: checking split 9/11 .* +// CHECK: checking split 10/11 .* +// CHECK: checking split 11/11 .* // CHECK-L: SplitOnEveryAssert.bpl(31,5): Error: this assertion could not be proved procedure Ex() returns (y: int) diff --git a/Test/test0/SplitOnEveryAssert.bpl b/Test/test0/SplitOnEveryAssert.bpl index d1313c7c9..e459892fd 100644 --- a/Test/test0/SplitOnEveryAssert.bpl +++ b/Test/test0/SplitOnEveryAssert.bpl @@ -3,18 +3,18 @@ // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: Verifying DoTheSplitting ... -// CHECK: checking split 1/12.* -// CHECK: checking split 2/12.* -// CHECK: checking split 3/12.* -// CHECK: checking split 4/12.* +// CHECK: checking split 1/11.* +// CHECK: checking split 2/11.* +// CHECK: checking split 3/11.* +// CHECK: checking split 4/11.* // CHECK: --> split #4 done, \[.* s\] Invalid -// CHECK: checking split 5/12.* -// CHECK: checking split 6/12.* -// CHECK: checking split 7/12.* -// CHECK: checking split 8/12.* -// CHECK: checking split 9/12.* -// CHECK: checking split 10/12.* -// CHECK: checking split 11/12.* +// CHECK: checking split 5/11.* +// CHECK: checking split 6/11.* +// CHECK: checking split 7/11.* +// CHECK: checking split 8/11.* +// CHECK: checking split 9/11.* +// CHECK: checking split 10/11.* +// CHECK: checking split 11/11.* // CHECK-L: SplitOnEveryAssert.bpl(36,5): Error: this assertion could not be proved // Verify the second procedure is NOT split. .* is necessary to match the blank line in-between. From 63a1088fe468ee1fd826901e0f2f5631b838cd7d Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sun, 13 Oct 2024 23:47:52 +0200 Subject: [PATCH 4/5] remove noop --- Source/VCGeneration/Splits/ManualSplitFinder.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs index 1d260a917..b1b8e676b 100644 --- a/Source/VCGeneration/Splits/ManualSplitFinder.cs +++ b/Source/VCGeneration/Splits/ManualSplitFinder.cs @@ -22,7 +22,7 @@ public static IEnumerable GetParts(VCGenOptions options, Implementa var splitParts = SplitAttributeHandler.GetParts(withoutIsolatedAssertions); var splits = isolatedJumps.Concat(isolatedAssertions).Concat(splitParts).Where(s => s.Asserts.Any()).ToList(); - return splits.ToList().Any() ? splits.ToList() : new List { focussedPart }; + return splits.Any() ? splits : new List { focussedPart }; }); return result; } From c345252d8e7d3d67501cc8732a1a9c48d8885848 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sun, 13 Oct 2024 23:51:35 +0200 Subject: [PATCH 5/5] actually fix test --- Test/commandline/SplitOnEveryAssert.bpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl index 19b275b60..50425d6e9 100644 --- a/Test/commandline/SplitOnEveryAssert.bpl +++ b/Test/commandline/SplitOnEveryAssert.bpl @@ -7,7 +7,7 @@ // CHECK: checking split 2/11 .* // CHECK: checking split 3/11 .* // CHECK: checking split 4/11 .* -// CHECK: --> split #3 done, \[.* s\] Invalid +// CHECK: --> split #4 done, \[.* s\] Invalid // CHECK: checking split 5/11 .* // CHECK: checking split 6/11 .* // CHECK: checking split 7/11 .*