Fix split printing (#996)

boogie-org · Jan 23, 2025 · c1b83b6 · c1b83b6
1 parent 7f9f784
commit c1b83b6
Show file tree

Hide file tree

Showing 10 changed files with 39 additions and 39 deletions.
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.4.3</Version>
+    <Version>3.4.4</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs
@@ -114,7 +114,7 @@ private void PrintSplit() {
           Thread.Sleep(100);
         }
 
-        var prefix = this is ManualSplit manualSplit ? manualSplit.Token.ShortName : "";
+        var prefix = this is ManualSplit manualSplit ? "-" + manualSplit.SplitIndex + manualSplit.Token.ShortName : "";
         var name = Implementation.Name + prefix; 
         using var writer = printToConsole
           ? new TokenTextWriter("<console>", Options.OutputWriter, false, Options.PrettyPrint, Options) 

diff --git a/Test/implementationDivision/focus/focus.bpl.expect b/Test/implementationDivision/focus/focus.bpl.expect
@@ -1,4 +1,4 @@
-implementation Ex() returns (y: int)
+implementation Ex-0() returns (y: int)
 {
 
   anon0:
@@ -13,7 +13,7 @@ implementation Ex() returns (y: int)
 }
 
 
-implementation Ex/focus[+16,-20,-25]/afterSplit@15() returns (y: int)
+implementation Ex-1/focus[+16,-20,-25]/afterSplit@15() returns (y: int)
 {
 
   anon0:
@@ -32,7 +32,7 @@ implementation Ex/focus[+16,-20,-25]/afterSplit@15() returns (y: int)
 }
 
 
-implementation Ex/focus[+16,-20,+25]() returns (y: int)
+implementation Ex-2/focus[+16,-20,+25]() returns (y: int)
 {
 
   anon0:
@@ -56,7 +56,7 @@ implementation Ex/focus[+16,-20,+25]() returns (y: int)
 }
 
 
-implementation Ex/focus[+16,+20,-25]() returns (y: int)
+implementation Ex-3/focus[+16,+20,-25]() returns (y: int)
 {
 
   anon0:
@@ -76,7 +76,7 @@ implementation Ex/focus[+16,+20,-25]() returns (y: int)
 }
 
 
-implementation Ex/focus[+16,+20,+25]() returns (y: int)
+implementation Ex-4/focus[+16,+20,+25]() returns (y: int)
 {
 
   anon0:
@@ -102,7 +102,7 @@ implementation Ex/focus[+16,+20,+25]() returns (y: int)
 
 
 focus.bpl(15,5): Error: this assertion could not be proved
-implementation focusInconsistency/focus[+38](x: int) returns (y: int)
+implementation focusInconsistency--1/focus[+38](x: int) returns (y: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect
@@ -1,4 +1,4 @@
-implementation IsolateAssertion/assert@20(x: int, y: int)
+implementation IsolateAssertion-0/assert@20(x: int, y: int)
 {
 
   anon0:
@@ -38,7 +38,7 @@ implementation IsolateAssertion/assert@20(x: int, y: int)
 }
 
 
-implementation IsolateAssertion(x: int, y: int)
+implementation IsolateAssertion-1(x: int, y: int)
 {
 
   anon0:
@@ -81,7 +81,7 @@ implementation IsolateAssertion(x: int, y: int)
 
 isolateAssertion.bpl(20,3): Error: this assertion could not be proved
 isolateAssertion.bpl(21,3): Error: this assertion could not be proved
-implementation IsolatePathsAssertion/assert@50/path[29,45](x: int, y: int)
+implementation IsolatePathsAssertion-0/assert@50/path[29,45](x: int, y: int)
 {
 
   anon0:
@@ -112,7 +112,7 @@ implementation IsolatePathsAssertion/assert@50/path[29,45](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/path[29,47](x: int, y: int)
+implementation IsolatePathsAssertion-1/assert@50/path[29,47](x: int, y: int)
 {
 
   anon0:
@@ -143,7 +143,7 @@ implementation IsolatePathsAssertion/assert@50/path[29,47](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/path[31,32,45](x: int, y: int)
+implementation IsolatePathsAssertion-2/assert@50/path[31,32,45](x: int, y: int)
 {
 
   anon0:
@@ -175,7 +175,7 @@ implementation IsolatePathsAssertion/assert@50/path[31,32,45](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/path[31,32,47](x: int, y: int)
+implementation IsolatePathsAssertion-3/assert@50/path[31,32,47](x: int, y: int)
 {
 
   anon0:
@@ -207,7 +207,7 @@ implementation IsolatePathsAssertion/assert@50/path[31,32,47](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/path[31,35,45](x: int, y: int)
+implementation IsolatePathsAssertion-4/assert@50/path[31,35,45](x: int, y: int)
 {
 
   anon0:
@@ -239,7 +239,7 @@ implementation IsolatePathsAssertion/assert@50/path[31,35,45](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/path[31,35,47](x: int, y: int)
+implementation IsolatePathsAssertion-5/assert@50/path[31,35,47](x: int, y: int)
 {
 
   anon0:
@@ -271,7 +271,7 @@ implementation IsolatePathsAssertion/assert@50/path[31,35,47](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion(x: int, y: int)
+implementation IsolatePathsAssertion-6(x: int, y: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect b/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect
@@ -1,4 +1,4 @@
-implementation IsolateContinue/remainingAssertions(x: int) returns (r: int)
+implementation IsolateContinue-0/remainingAssertions(x: int) returns (r: int)
 {
 
   anon0:
@@ -26,7 +26,7 @@ implementation IsolateContinue/remainingAssertions(x: int) returns (r: int)
 }
 
 
-implementation IsolateContinue/goto@17(x: int) returns (r: int)
+implementation IsolateContinue-1/goto@17(x: int) returns (r: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect
@@ -1,4 +1,4 @@
-implementation IsolateReturn/remainingAssertions(x: int, y: int) returns (r: int)
+implementation IsolateReturn-0/remainingAssertions(x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -25,7 +25,7 @@ implementation IsolateReturn/remainingAssertions(x: int, y: int) returns (r: int
 }
 
 
-implementation IsolateReturn/return@16(x: int, y: int) returns (r: int)
+implementation IsolateReturn-1/return@16(x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -54,7 +54,7 @@ implementation IsolateReturn/return@16(x: int, y: int) returns (r: int)
 
 isolateJump.bpl(16,21): Error: a postcondition could not be proved on this return path
 isolateJump.bpl(5,3): Related location: this is the postcondition that could not be proved
-implementation IsolateReturnPaths/remainingAssertions(x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-0/remainingAssertions(x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -98,7 +98,7 @@ implementation IsolateReturnPaths/remainingAssertions(x: int, y: int) returns (r
 }
 
 
-implementation IsolateReturnPaths/return@44/path[27](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-1/return@44/path[27](x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -125,7 +125,7 @@ implementation IsolateReturnPaths/return@44/path[27](x: int, y: int) returns (r:
 }
 
 
-implementation IsolateReturnPaths/return@44/path[29,30](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-2/return@44/path[29,30](x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -153,7 +153,7 @@ implementation IsolateReturnPaths/return@44/path[29,30](x: int, y: int) returns
 }
 
 
-implementation IsolateReturnPaths/return@44/path[29,33](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-3/return@44/path[29,33](x: int, y: int) returns (r: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect b/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect
@@ -1,4 +1,4 @@
-implementation {:vcs_split_on_every_assert} MergeAtEnd/assert@5(x: int) returns (r: int)
+implementation {:vcs_split_on_every_assert} MergeAtEnd--1/assert@5(x: int) returns (r: int)
 {
 
   anon0:
@@ -22,7 +22,7 @@ implementation {:vcs_split_on_every_assert} MergeAtEnd/assert@5(x: int) returns
 
 isolateJumpAndSplitOnEveryAssert.bpl(9,3): Error: a postcondition could not be proved on this return path
 isolateJumpAndSplitOnEveryAssert.bpl(5,3): Related location: this is the postcondition that could not be proved
-implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@16(x: int) returns (r: int)
+implementation {:vcs_split_on_every_assert} MultipleEnsures-0/return@25/assert@16(x: int) returns (r: int)
 {
 
   anon0:
@@ -33,7 +33,7 @@ implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@16(
 }
 
 
-implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@17(x: int) returns (r: int)
+implementation {:vcs_split_on_every_assert} MultipleEnsures-1/return@25/assert@17(x: int) returns (r: int)
 {
 
   anon0:
@@ -45,7 +45,7 @@ implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@17(
 }
 
 
-implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@16(x: int) returns (r: int)
+implementation {:vcs_split_on_every_assert} MultipleEnsures-2/return@21/assert@16(x: int) returns (r: int)
 {
 
   anon0:
@@ -56,7 +56,7 @@ implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@16(
 }
 
 
-implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@17(x: int) returns (r: int)
+implementation {:vcs_split_on_every_assert} MultipleEnsures-3/return@21/assert@17(x: int) returns (r: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect
@@ -1,4 +1,4 @@
-implementation Foo/untilFirstSplit()
+implementation Foo-0/untilFirstSplit()
 {
 
   anon3_Then:
@@ -8,7 +8,7 @@ implementation Foo/untilFirstSplit()
 }
 
 
-implementation Foo/afterSplit@11()
+implementation Foo-1/afterSplit@11()
 {
 
   anon3_Else:
@@ -20,7 +20,7 @@ implementation Foo/afterSplit@11()
 }
 
 
-implementation Foo/afterSplit@12()
+implementation Foo-2/afterSplit@12()
 {
 
   anon3_Else:

diff --git a/Test/implementationDivision/split/Split.bpl.expect b/Test/implementationDivision/split/Split.bpl.expect
@@ -1,4 +1,4 @@
-implementation Foo/untilFirstSplit() returns (y: int)
+implementation Foo-0/untilFirstSplit() returns (y: int)
 {
 
   anon0:
@@ -13,7 +13,7 @@ implementation Foo/untilFirstSplit() returns (y: int)
 }
 
 
-implementation Foo/afterSplit@15() returns (y: int)
+implementation Foo-1/afterSplit@15() returns (y: int)
 {
 
   anon0:
@@ -32,7 +32,7 @@ implementation Foo/afterSplit@15() returns (y: int)
 }
 
 
-implementation Foo/afterSplit@22() returns (y: int)
+implementation Foo-2/afterSplit@22() returns (y: int)
 {
 
   anon0:
@@ -51,7 +51,7 @@ implementation Foo/afterSplit@22() returns (y: int)
 }
 
 
-implementation Foo/afterSplit@25() returns (y: int)
+implementation Foo-3/afterSplit@25() returns (y: int)
 {
 
   anon0:
@@ -86,7 +86,7 @@ implementation Foo/afterSplit@25() returns (y: int)
 }
 
 
-implementation Foo/afterSplit@19() returns (y: int)
+implementation Foo-4/afterSplit@19() returns (y: int)
 {
 
   anon0:

diff --git a/Test/pruning/MonomorphicSplit.bpl b/Test/pruning/MonomorphicSplit.bpl
@@ -1,5 +1,5 @@
 // RUN: %parallel-boogie /prune:1 /errorTrace:0 /printSplit:"%t" /printSplitDeclarations "%s" > "%t"
-// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit.spl"
+// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit--1.spl"
 
 // The following checks are a bit simplistic, but this is
 // on purpose to reduce brittleness. We assume there would now be two uses clauses