summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Test/lazyinline/Answer92
-rw-r--r--Test/lazyinline/bar1.bpl26
-rw-r--r--Test/lazyinline/bar2.bpl24
-rw-r--r--Test/lazyinline/bar3.bpl41
-rw-r--r--Test/lazyinline/bar4.bpl38
-rw-r--r--Test/lazyinline/bar5.bpl26
-rw-r--r--Test/lazyinline/bar6.bpl36
-rw-r--r--Test/lazyinline/bar7.bpl27
-rw-r--r--Test/lazyinline/bar8.bpl16
-rw-r--r--Test/lazyinline/foo.bpl30
-rw-r--r--Test/lazyinline/fooret.bpl36
-rw-r--r--Test/lazyinline/runtest.bat33
12 files changed, 0 insertions, 425 deletions
diff --git a/Test/lazyinline/Answer b/Test/lazyinline/Answer
deleted file mode 100644
index eb3baae3..00000000
--- a/Test/lazyinline/Answer
+++ /dev/null
@@ -1,92 +0,0 @@
------ Running regression test bar1.bpl
-bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
-bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
-Execution trace:
- bar1.bpl(24,3): anon0
- Inlined call to procedure foo begins
- bar1.bpl(13,5): anon0
- Inlined call to procedure bar begins
- bar1.bpl(7,5): anon0
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar1.bpl(7,5): anon0
- Inlined call to procedure bar ends
- Inlined call to procedure foo ends
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar2.bpl
-bar2.bpl(21,3): Error BP5001: This assertion might not hold.
-Execution trace:
- bar2.bpl(19,3): anon0
- Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(6,7): anon3_Then
- Inlined call to procedure foo ends
- Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(9,7): anon3_Else
- Inlined call to procedure foo ends
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar3.bpl
-bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
-bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
-Execution trace:
- bar3.bpl(38,3): anon0
- Inlined call to procedure foo begins
- bar3.bpl(18,3): anon0
- bar3.bpl(19,7): anon3_Then
- Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(8,7): anon3_Then
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(8,7): anon3_Then
- Inlined call to procedure bar ends
- Inlined call to procedure foo ends
- Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(10,7): anon3_Else
- Inlined call to procedure bar ends
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar4.bpl
-
-Boogie program verifier finished with 1 verified, 0 errors
------
------ Running regression test bar5.bpl
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar5.bpl(24,3): anon0
- Inlined call to procedure foo begins
- bar5.bpl(13,5): anon0
- Inlined call to procedure foo ends
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar6.bpl
-
-Boogie program verifier finished with 1 verified, 0 errors
------
------ Running regression test bar7.bpl
-
-Boogie program verifier finished with 1 verified, 0 errors
------
------ Running regression test bar8.bpl
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar8.bpl(13,5): anon0
- Inlined call to procedure foo begins
- bar8.bpl(6,3): anon0
- Inlined call to procedure foo ends
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test foo.bpl
-
-Boogie program verifier finished with 2 verified, 0 errors
------
diff --git a/Test/lazyinline/bar1.bpl b/Test/lazyinline/bar1.bpl
deleted file mode 100644
index 845954d5..00000000
--- a/Test/lazyinline/bar1.bpl
+++ /dev/null
@@ -1,26 +0,0 @@
-var x: int;
-var y: int;
-
-procedure {:inline 1} bar()
-modifies y;
-{
- y := y + 1;
-}
-
-procedure {:inline 1} foo()
-modifies x, y;
-{
- x := x + 1;
- call bar();
- call bar();
- x := x + 1;
-}
-
-procedure main()
-requires x == y;
-ensures x != y;
-modifies x, y;
-{
- call foo();
-}
-
diff --git a/Test/lazyinline/bar2.bpl b/Test/lazyinline/bar2.bpl
deleted file mode 100644
index 76991a8f..00000000
--- a/Test/lazyinline/bar2.bpl
+++ /dev/null
@@ -1,24 +0,0 @@
-
-procedure {:inline 1} foo() returns (x: bool)
-{
- var b: bool;
- if (b) {
- x := false;
- return;
- } else {
- x := true;
- return;
- }
-}
-
-procedure main()
-{
- var b1: bool;
- var b2: bool;
-
- call b1 := foo();
- call b2 := foo();
- assert b1 == b2;
-}
-
-
diff --git a/Test/lazyinline/bar3.bpl b/Test/lazyinline/bar3.bpl
deleted file mode 100644
index 7bd91184..00000000
--- a/Test/lazyinline/bar3.bpl
+++ /dev/null
@@ -1,41 +0,0 @@
-var y: int;
-var x: int;
-
-procedure {:inline 1} bar(b: bool)
-modifies y;
-{
- if (b) {
- y := y + 1;
- } else {
- y := y - 1;
- }
-}
-
-procedure {:inline 1} foo()
-modifies x, y;
-{
- var b: bool;
- if (b) {
- x := x + 1;
- call bar(true);
- call bar(true);
- x := x + 1;
- } else {
- x := x - 1;
- call bar(false);
- call bar(false);
- x := x - 1;
- }
-}
-
-
-procedure main()
-requires x == y;
-ensures x == y;
-modifies x, y;
-modifies y;
-{
- call foo();
- assert x == y;
- call bar(false);
-}
diff --git a/Test/lazyinline/bar4.bpl b/Test/lazyinline/bar4.bpl
deleted file mode 100644
index 84640811..00000000
--- a/Test/lazyinline/bar4.bpl
+++ /dev/null
@@ -1,38 +0,0 @@
-var y: int;
-var x: int;
-
-procedure {:inline 1} bar() returns (b: bool)
-modifies y;
-{
- if (b) {
- y := y + 1;
- } else {
- y := y - 1;
- }
-}
-
-procedure {:inline 1} foo()
-modifies x, y;
-{
- var b: bool;
-
- call b := bar();
- if (b) {
- x := x + 1;
- } else {
- x := x - 1;
- }
-}
-
-
-procedure main() returns (b: bool)
-requires x == y;
-ensures !b ==> x == y+1;
-ensures b ==> x+1 == y;
-modifies x, y;
-modifies y;
-{
- call foo();
- assert x == y;
- call b := bar();
-}
diff --git a/Test/lazyinline/bar5.bpl b/Test/lazyinline/bar5.bpl
deleted file mode 100644
index ec399b4a..00000000
--- a/Test/lazyinline/bar5.bpl
+++ /dev/null
@@ -1,26 +0,0 @@
-var x: int;
-var y: int;
-
-procedure {:inline 1} bar()
-modifies y;
-{
- y := y + 1;
-}
-
-procedure {:inline 1} foo()
-modifies x, y;
-{
- x := x + 1;
- assert x == y;
- call bar();
- call bar();
- x := x + 1;
-}
-
-procedure main()
-requires x == y;
-modifies x, y;
-{
- call foo();
-}
-
diff --git a/Test/lazyinline/bar6.bpl b/Test/lazyinline/bar6.bpl
deleted file mode 100644
index e133aef7..00000000
--- a/Test/lazyinline/bar6.bpl
+++ /dev/null
@@ -1,36 +0,0 @@
-var M: [int]int;
-
-procedure {:inline 1} bar(y: int) returns (b: bool)
-modifies M;
-{
- if (b) {
- M[y] := M[y] + 1;
- } else {
- M[y] := M[y] - 1;
- }
-}
-
-procedure {:inline 1} foo(x: int, y: int)
-modifies M;
-{
- var b: bool;
-
- call b := bar(y);
- if (b) {
- M[x] := M[x] + 1;
- } else {
- M[x] := M[x] - 1;
- }
-}
-
-procedure main(x: int, y: int) returns (b: bool)
-requires x != y;
-requires M[x] == M[y];
-ensures !b ==> M[x] == M[y]+1;
-ensures b ==> M[x]+1 == M[y];
-modifies M;
-{
- call foo(x, y);
- assert M[x] == M[y];
- call b := bar(y);
-}
diff --git a/Test/lazyinline/bar7.bpl b/Test/lazyinline/bar7.bpl
deleted file mode 100644
index 0eff6a7d..00000000
--- a/Test/lazyinline/bar7.bpl
+++ /dev/null
@@ -1,27 +0,0 @@
-var x: int;
-var y: int;
-
-procedure {:inline 1} bar()
-modifies y;
-{
- y := y + 1;
-}
-
-procedure {:inline 1} foo()
-modifies x, y;
-{
- x := x + 1;
- assert x != y;
- call bar();
- call bar();
- x := x + 1;
- assert x == y;
-}
-
-procedure main()
-requires x == y;
-modifies x, y;
-{
- call foo();
-}
-
diff --git a/Test/lazyinline/bar8.bpl b/Test/lazyinline/bar8.bpl
deleted file mode 100644
index dd6dab31..00000000
--- a/Test/lazyinline/bar8.bpl
+++ /dev/null
@@ -1,16 +0,0 @@
-var x: int;
-var y: int;
-
-procedure {:inline 1} foo()
-{
- assert x == y;
-}
-
-procedure main()
-requires x == y;
-modifies x, y;
-{
- x := x + 1;
- call foo();
-}
-
diff --git a/Test/lazyinline/foo.bpl b/Test/lazyinline/foo.bpl
deleted file mode 100644
index bd45258a..00000000
--- a/Test/lazyinline/foo.bpl
+++ /dev/null
@@ -1,30 +0,0 @@
-var g: int;
-
-procedure A()
-requires g == 0;
-modifies g;
-ensures g == 2;
-{
- var x : int;
- x := 4;
- while (g < x) {
- g := g + 1;
- x := x - 1;
- }
- assert x == 2;
-}
-
-procedure B(j: int) returns (x: int)
-{
- var i: int;
- var y: int;
-
- y := 0;
- i := 0;
- x := j;
- while (i < 100) {
- x := x + 1 + y;
- i := i + 1;
- }
- assert y == 0;
-}
diff --git a/Test/lazyinline/fooret.bpl b/Test/lazyinline/fooret.bpl
deleted file mode 100644
index c81baaf1..00000000
--- a/Test/lazyinline/fooret.bpl
+++ /dev/null
@@ -1,36 +0,0 @@
-
-procedure A()
-{
- var x : int;
- var y : int;
- var nondet: bool;
-
-start:
- x := 0;
- assume y == 2;
- goto lh;
-
-lh:
- goto lab1, lab2;
-
-lab1:
- assume x < y;
- x := x + 1;
- havoc nondet;
- goto lab3, lab4;
-
-lab3:
- assume !nondet;
- goto lh;
-
-lab4:
- assume nondet;
- return;
-
-lab2:
- assume x >= y;
- assert false;
-
-}
-
-
diff --git a/Test/lazyinline/runtest.bat b/Test/lazyinline/runtest.bat
deleted file mode 100644
index e7e86446..00000000
--- a/Test/lazyinline/runtest.bat
+++ /dev/null
@@ -1,33 +0,0 @@
-@echo off
-setlocal
-
-set BGEXE=..\..\Binaries\Boogie.exe
-rem set BGEXE=mono ..\..\Binaries\Boogie.exe
-
-echo ----- Running regression test bar1.bpl
-%BGEXE% %* /noinfer /lazyInline:1 bar1.bpl
-echo -----
-echo ----- Running regression test bar2.bpl
-%BGEXE% %* /noinfer /lazyInline:1 bar2.bpl
-echo -----
-echo ----- Running regression test bar3.bpl
-%BGEXE% %* /noinfer /lazyInline:1 bar3.bpl
-echo -----
-echo ----- Running regression test bar4.bpl
-%BGEXE% %* /noinfer /lazyInline:1 bar4.bpl
-echo -----
-echo ----- Running regression test bar5.bpl
-%BGEXE% %* /noinfer /lazyInline:1 bar5.bpl
-echo -----
-echo ----- Running regression test bar6.bpl
-%BGEXE% %* /noinfer /lazyInline:1 bar6.bpl
-echo -----
-echo ----- Running regression test bar7.bpl
-%BGEXE% %* /noinfer /lazyInline:1 bar7.bpl
-echo -----
-echo ----- Running regression test bar8.bpl
-%BGEXE% %* /noinfer /lazyInline:1 bar8.bpl
-echo -----
-echo ----- Running regression test foo.bpl
-%BGEXE% %* /noinfer /lazyInline:1 /extractLoops foo.bpl
-echo -----
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-29 20:58:09 +0000