Test file fixes

boogie-org · Oct 2, 2024 · a7ce5e0 · a7ce5e0
1 parent 064b44a
commit a7ce5e0
Show file tree

Hide file tree

Showing 15 changed files with 151 additions and 170 deletions.
diff --git a/...lit/assumeFalseSplit/AssumeFalseSplit.bpl → ...tationDivision/split/AssumeFalseSplit.bpl b/...lit/assumeFalseSplit/AssumeFalseSplit.bpl → ...tationDivision/split/AssumeFalseSplit.bpl
@@ -1,8 +1,5 @@
-// RUN: %parallel-boogie /printSplit:%t "%s" > "%t"
+// RUN: %boogie /printSplit:- "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-// RUN: %diff %S/Foo.split.0.bpl.expect %t-Foo-0.spl
-// RUN: %diff %S/Foo.split.1.bpl.expect %t-Foo-1.spl
-// RUN: %diff %S/Foo.split.2.bpl.expect %t-Foo-2.spl
 
 procedure Foo()
 {

diff --git a/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect
@@ -0,0 +1,36 @@
+implementation Foo/split@4()
+{
+
+  anon3_Then:
+    assert 2 == 1 + 1;
+    assume false;
+    return;
+}
+
+
+implementation Foo/split@11()
+{
+
+  anon3_Else:
+    assume 2 == 1 + 1;
+    assert {:split_here} 2 == 2;
+    assume 3 == 2 + 1;
+    assume 1 == 1;
+    goto ;
+}
+
+
+implementation Foo/split@12()
+{
+
+  anon3_Else:
+    assume 2 == 1 + 1;
+    assume 2 == 2;
+    assert {:split_here} 3 == 2 + 1;
+    assert 1 == 1;
+    goto ;
+}
+
+
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/...ionDivision/split/originalSplit/Split.bpl → Test/implementationDivision/split/Split.bpl b/...ionDivision/split/originalSplit/Split.bpl → Test/implementationDivision/split/Split.bpl
@@ -1,9 +1,5 @@
-// RUN: %parallel-boogie /printSplit:%t "%s" > "%t"
+// RUN: %boogie /printSplit:- "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-// RUN: %diff %S/Foo.split.0.bpl.expect %t-Foo-0.spl
-// RUN: %diff %S/Foo.split.1.bpl.expect %t-Foo-1.spl
-// RUN: %diff %S/Foo.split.2.bpl.expect %t-Foo-2.spl
-// RUN: %diff %S/Foo.split.3.bpl.expect %t-Foo-3.spl
 
 procedure Foo() returns (y: int)
   ensures y >= 0;

diff --git a/Test/implementationDivision/split/Split.bpl.expect b/Test/implementationDivision/split/Split.bpl.expect
@@ -0,0 +1,112 @@
+implementation Foo/split@4() returns (y: int)
+{
+
+  anon0:
+    assert 5 + 0 == 5;
+    assert 5 * 5 <= 25;
+    assume x#AT#0 + y#AT#0 == 5;
+    assume x#AT#0 * x#AT#0 <= 25;
+    assume {:partition} 0 >= x#AT#0;
+    assume y#AT#2 == y#AT#0;
+    assert y#AT#2 >= 0;
+    return;
+}
+
+
+implementation Foo/split@15() returns (y: int)
+{
+
+  anon0:
+    assume 5 + 0 == 5;
+    assume 5 * 5 <= 25;
+    assume x#AT#0 + y#AT#0 == 5;
+    assume x#AT#0 * x#AT#0 <= 25;
+    assume {:partition} x#AT#0 > 0;
+    assume x#AT#1 == x#AT#0 - 1;
+    assert {:split_here} (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25;
+    assume y#AT#1 == y#AT#0 + 1;
+    assume {:partition} x#AT#1 < 3;
+    assert 2 < 2;
+    assume y#AT#1 * y#AT#1 > 4;
+    goto ;
+}
+
+
+implementation Foo/split@19() returns (y: int)
+{
+
+  anon0:
+    assume 5 + 0 == 5;
+    assume 5 * 5 <= 25;
+    assume x#AT#0 + y#AT#0 == 5;
+    assume x#AT#0 * x#AT#0 <= 25;
+    assume {:partition} x#AT#0 > 0;
+    assume x#AT#1 == x#AT#0 - 1;
+    assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25;
+    assume y#AT#1 == y#AT#0 + 1;
+    assume {:partition} x#AT#1 < 3;
+    assume 2 < 2;
+    assert {:split_here} y#AT#1 * y#AT#1 > 4;
+    goto ;
+}
+
+
+implementation Foo/split@22() returns (y: int)
+{
+
+  anon0:
+    assume 5 + 0 == 5;
+    assume 5 * 5 <= 25;
+    assume x#AT#0 + y#AT#0 == 5;
+    assume x#AT#0 * x#AT#0 <= 25;
+    assume {:partition} x#AT#0 > 0;
+    assume x#AT#1 == x#AT#0 - 1;
+    assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25;
+    assume y#AT#1 == y#AT#0 + 1;
+    assume {:partition} 3 <= x#AT#1;
+    assert {:split_here} y#AT#1 * y#AT#1 * y#AT#1 < 8;
+    assert 2 < 2;
+    goto ;
+}
+
+
+implementation Foo/split@25() returns (y: int)
+{
+
+  anon0:
+    assume 5 + 0 == 5;
+    assume 5 * 5 <= 25;
+    assume x#AT#0 + y#AT#0 == 5;
+    assume x#AT#0 * x#AT#0 <= 25;
+    assume {:partition} x#AT#0 > 0;
+    assume x#AT#1 == x#AT#0 - 1;
+    assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25;
+    assume y#AT#1 == y#AT#0 + 1;
+    goto anon6_Then, anon6_Else;
+
+  anon6_Then:
+    assume {:partition} x#AT#1 < 3;
+    assume 2 < 2;
+    assume y#AT#1 * y#AT#1 > 4;
+    goto anon4;
+
+  anon6_Else:
+    assume {:partition} 3 <= x#AT#1;
+    assume y#AT#1 * y#AT#1 * y#AT#1 < 8;
+    assume 2 < 2;
+    goto anon4;
+
+  anon4:
+    assert {:split_here} (x#AT#1 + y#AT#1) * (x#AT#1 + y#AT#1) == 25;
+    assert x#AT#1 + y#AT#1 == 5;
+    assert x#AT#1 * x#AT#1 <= 25;
+    assume false;
+    return;
+}
+
+
+Split.bpl(15,5): Error: this assertion could not be proved
+Execution trace:
+    Split.bpl(8,5): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/implementationDivision/split/assumeFalseSplit/AssumeFalseSplit.bpl.expect b/Test/implementationDivision/split/assumeFalseSplit/AssumeFalseSplit.bpl.expect
diff --git a/Test/implementationDivision/split/assumeFalseSplit/Foo.split.0.bpl.expect b/Test/implementationDivision/split/assumeFalseSplit/Foo.split.0.bpl.expect
diff --git a/Test/implementationDivision/split/assumeFalseSplit/Foo.split.1.bpl.expect b/Test/implementationDivision/split/assumeFalseSplit/Foo.split.1.bpl.expect
diff --git a/Test/implementationDivision/split/assumeFalseSplit/Foo.split.2.bpl.expect b/Test/implementationDivision/split/assumeFalseSplit/Foo.split.2.bpl.expect
diff --git a/Test/implementationDivision/split/originalSplit/Foo.split.0.bpl.expect b/Test/implementationDivision/split/originalSplit/Foo.split.0.bpl.expect
diff --git a/Test/implementationDivision/split/originalSplit/Foo.split.1.bpl.expect b/Test/implementationDivision/split/originalSplit/Foo.split.1.bpl.expect
diff --git a/Test/implementationDivision/split/originalSplit/Foo.split.2.bpl.expect b/Test/implementationDivision/split/originalSplit/Foo.split.2.bpl.expect
diff --git a/Test/implementationDivision/split/originalSplit/Foo.split.3.bpl.expect b/Test/implementationDivision/split/originalSplit/Foo.split.3.bpl.expect
diff --git a/Test/implementationDivision/split/originalSplit/Foo.split.4.bpl.expect b/Test/implementationDivision/split/originalSplit/Foo.split.4.bpl.expect
diff --git a/Test/implementationDivision/split/originalSplit/Split.bpl.expect b/Test/implementationDivision/split/originalSplit/Split.bpl.expect
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--1.spl"
+// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit.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