Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: Skip empty splits #965

Merged
merged 5 commits into from
Oct 14, 2024
Merged

fix: Skip empty splits #965

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
e426c84
try filtering the splits
fabiomadge Oct 13, 2024
f303d01
revert unit test
fabiomadge Oct 13, 2024
ddf8498
revert more tests
fabiomadge Oct 13, 2024
63a1088
remove noop
fabiomadge Oct 13, 2024
c345252
actually fix test
fabiomadge Oct 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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> { SolverOutcome.Invalid, SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid };
for (var index = 0; index < outcomes.Count; index++)
Expand Down
3 changes: 2 additions & 1 deletion Source/VCGeneration/Splits/ManualSplitFinder.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,8 @@ public static IEnumerable<ManualSplit> 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.Any() ? splits : new List<ManualSplit> { focussedPart };
});
return result;
}
Expand Down
22 changes: 11 additions & 11 deletions Test/commandline/SplitOnEveryAssert.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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: 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(31,5): Error: this assertion could not be proved

procedure Ex() returns (y: int)
Expand Down
22 changes: 11 additions & 11 deletions Test/test0/SplitOnEveryAssert.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading