From a7ce5e06dd91bd5fe947391dcbaa82c6ba581829 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 2 Oct 2024 16:52:08 +0200 Subject: [PATCH] Test file fixes --- .../AssumeFalseSplit.bpl | 5 +- .../split/AssumeFalseSplit.bpl.expect | 36 ++++++ .../split/{originalSplit => }/Split.bpl | 6 +- .../split/Split.bpl.expect | 112 ++++++++++++++++++ .../AssumeFalseSplit.bpl.expect | 2 - .../assumeFalseSplit/Foo.split.0.bpl.expect | 10 -- .../assumeFalseSplit/Foo.split.1.bpl.expect | 12 -- .../assumeFalseSplit/Foo.split.2.bpl.expect | 12 -- .../originalSplit/Foo.split.0.bpl.expect | 15 --- .../originalSplit/Foo.split.1.bpl.expect | 19 --- .../originalSplit/Foo.split.2.bpl.expect | 19 --- .../originalSplit/Foo.split.3.bpl.expect | 35 ------ .../originalSplit/Foo.split.4.bpl.expect | 31 ----- .../split/originalSplit/Split.bpl.expect | 5 - Test/pruning/MonomorphicSplit.bpl | 2 +- 15 files changed, 151 insertions(+), 170 deletions(-) rename Test/implementationDivision/split/{assumeFalseSplit => }/AssumeFalseSplit.bpl (50%) create mode 100644 Test/implementationDivision/split/AssumeFalseSplit.bpl.expect rename Test/implementationDivision/split/{originalSplit => }/Split.bpl (64%) create mode 100644 Test/implementationDivision/split/Split.bpl.expect delete mode 100644 Test/implementationDivision/split/assumeFalseSplit/AssumeFalseSplit.bpl.expect delete mode 100644 Test/implementationDivision/split/assumeFalseSplit/Foo.split.0.bpl.expect delete mode 100644 Test/implementationDivision/split/assumeFalseSplit/Foo.split.1.bpl.expect delete mode 100644 Test/implementationDivision/split/assumeFalseSplit/Foo.split.2.bpl.expect delete mode 100644 Test/implementationDivision/split/originalSplit/Foo.split.0.bpl.expect delete mode 100644 Test/implementationDivision/split/originalSplit/Foo.split.1.bpl.expect delete mode 100644 Test/implementationDivision/split/originalSplit/Foo.split.2.bpl.expect delete mode 100644 Test/implementationDivision/split/originalSplit/Foo.split.3.bpl.expect delete mode 100644 Test/implementationDivision/split/originalSplit/Foo.split.4.bpl.expect delete mode 100644 Test/implementationDivision/split/originalSplit/Split.bpl.expect diff --git a/Test/implementationDivision/split/assumeFalseSplit/AssumeFalseSplit.bpl b/Test/implementationDivision/split/AssumeFalseSplit.bpl similarity index 50% rename from Test/implementationDivision/split/assumeFalseSplit/AssumeFalseSplit.bpl rename to Test/implementationDivision/split/AssumeFalseSplit.bpl index 148216280..92c6bb87f 100644 --- a/Test/implementationDivision/split/assumeFalseSplit/AssumeFalseSplit.bpl +++ b/Test/implementationDivision/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 new file mode 100644 index 000000000..29725f4eb --- /dev/null +++ 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/Test/implementationDivision/split/originalSplit/Split.bpl b/Test/implementationDivision/split/Split.bpl similarity index 64% rename from Test/implementationDivision/split/originalSplit/Split.bpl rename to Test/implementationDivision/split/Split.bpl index e99d76351..4c7fdaf45 100644 --- a/Test/implementationDivision/split/originalSplit/Split.bpl +++ b/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 new file mode 100644 index 000000000..c8b6615c9 --- /dev/null +++ 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 deleted file mode 100644 index 37fad75c9..000000000 --- a/Test/implementationDivision/split/assumeFalseSplit/AssumeFalseSplit.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/implementationDivision/split/assumeFalseSplit/Foo.split.0.bpl.expect b/Test/implementationDivision/split/assumeFalseSplit/Foo.split.0.bpl.expect deleted file mode 100644 index c8727ad27..000000000 --- a/Test/implementationDivision/split/assumeFalseSplit/Foo.split.0.bpl.expect +++ /dev/null @@ -1,10 +0,0 @@ -implementation Foo() -{ - - anon3_Then: - assert 2 == 1 + 1; - assume false; - return; -} - - diff --git a/Test/implementationDivision/split/assumeFalseSplit/Foo.split.1.bpl.expect b/Test/implementationDivision/split/assumeFalseSplit/Foo.split.1.bpl.expect deleted file mode 100644 index 29ba05d16..000000000 --- a/Test/implementationDivision/split/assumeFalseSplit/Foo.split.1.bpl.expect +++ /dev/null @@ -1,12 +0,0 @@ -implementation Foo() -{ - - anon3_Else: - assume 2 == 1 + 1; - assert {:split_here} 2 == 2; - assume 3 == 2 + 1; - assume 1 == 1; - goto ; -} - - diff --git a/Test/implementationDivision/split/assumeFalseSplit/Foo.split.2.bpl.expect b/Test/implementationDivision/split/assumeFalseSplit/Foo.split.2.bpl.expect deleted file mode 100644 index 838d5aebd..000000000 --- a/Test/implementationDivision/split/assumeFalseSplit/Foo.split.2.bpl.expect +++ /dev/null @@ -1,12 +0,0 @@ -implementation Foo() -{ - - anon3_Else: - assume 2 == 1 + 1; - assume 2 == 2; - assert {:split_here} 3 == 2 + 1; - assert 1 == 1; - goto ; -} - - diff --git a/Test/implementationDivision/split/originalSplit/Foo.split.0.bpl.expect b/Test/implementationDivision/split/originalSplit/Foo.split.0.bpl.expect deleted file mode 100644 index 79578bccc..000000000 --- a/Test/implementationDivision/split/originalSplit/Foo.split.0.bpl.expect +++ /dev/null @@ -1,15 +0,0 @@ -implementation Foo() 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; -} - - diff --git a/Test/implementationDivision/split/originalSplit/Foo.split.1.bpl.expect b/Test/implementationDivision/split/originalSplit/Foo.split.1.bpl.expect deleted file mode 100644 index 37297e028..000000000 --- a/Test/implementationDivision/split/originalSplit/Foo.split.1.bpl.expect +++ /dev/null @@ -1,19 +0,0 @@ -implementation Foo() 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 ; -} - - diff --git a/Test/implementationDivision/split/originalSplit/Foo.split.2.bpl.expect b/Test/implementationDivision/split/originalSplit/Foo.split.2.bpl.expect deleted file mode 100644 index 7f28a2ebf..000000000 --- a/Test/implementationDivision/split/originalSplit/Foo.split.2.bpl.expect +++ /dev/null @@ -1,19 +0,0 @@ -implementation Foo() 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 ; -} - - diff --git a/Test/implementationDivision/split/originalSplit/Foo.split.3.bpl.expect b/Test/implementationDivision/split/originalSplit/Foo.split.3.bpl.expect deleted file mode 100644 index eb031aa38..000000000 --- a/Test/implementationDivision/split/originalSplit/Foo.split.3.bpl.expect +++ /dev/null @@ -1,35 +0,0 @@ -implementation Foo() 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_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; - - anon6_Then: - assume {:partition} x#AT#1 < 3; - assume 2 < 2; - assume y#AT#1 * y#AT#1 > 4; - goto anon4; -} - - diff --git a/Test/implementationDivision/split/originalSplit/Foo.split.4.bpl.expect b/Test/implementationDivision/split/originalSplit/Foo.split.4.bpl.expect deleted file mode 100644 index 83b9850a7..000000000 --- a/Test/implementationDivision/split/originalSplit/Foo.split.4.bpl.expect +++ /dev/null @@ -1,31 +0,0 @@ -implementation Foo() returns (y: int) -{ - - PreconditionGeneratedEntry: - goto anon0; - - anon0: - assume 5 + 0 == 5; - assume 5 * 5 <= 25; - goto anon5_LoopHead; - - anon5_LoopHead: - assume x#AT#0 + y#AT#0 == 5; - assume x#AT#0 * x#AT#0 <= 25; - goto anon5_LoopBody; - - anon5_LoopBody: - 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_Then: - assume {:partition} x#AT#1 < 3; - assume 2 < 2; - assert {:split_here} y#AT#1 * y#AT#1 > 4; - goto ; -} - - diff --git a/Test/implementationDivision/split/originalSplit/Split.bpl.expect b/Test/implementationDivision/split/originalSplit/Split.bpl.expect deleted file mode 100644 index 67f8e9921..000000000 --- a/Test/implementationDivision/split/originalSplit/Split.bpl.expect +++ /dev/null @@ -1,5 +0,0 @@ -Split.bpl(19,5): Error: this assertion could not be proved -Execution trace: - Split.bpl(12,5): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/pruning/MonomorphicSplit.bpl b/Test/pruning/MonomorphicSplit.bpl index 15351bb11..1fccbd8bf 100644 --- 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