removed the lazy inline test directory

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 -----