Boogie: Added boolean code expressions (sans well-formedness checks on the input).

7 files changed, 239 insertions, 12 deletions

diff --git a/Test/alltests.txt b/Test/alltests.txt
index 588a5eda..4b12e6fd 100644
--- a/Test/alltests.txt
+++ b/Test/alltests.txt
@@ -1,4 +1,4 @@
-sanity		 Use    Build stability test - makes sure the current build doesn't encounter a runtime error (a smoke test)

+sanity           Use    Build stability test - makes sure the current build doesn't encounter a runtime error (a smoke test)

 test0            Use    Name resolution tests

 test1            Use    Typechecking tests

 test2            Use    VC generation

@@ -15,15 +15,16 @@ textbook         Use    Some textbook examples
 test15           Use    Benchmarks for error messages

 bitvectors       Use    Smoke tests for bitvectors

 smoke            Use    Soundness smoke testing

-test16           Use    Tests methodology of visible-state semantics and loop unrolling

+test16           Use    Tests loop unrolling

+codeexpr         Use    Tests code expressions

 test17           Postponed    Tests inference of parameterized contracts

 z3api            Postponed    Test for Z3 Managed .NET API prover

 houdini          Postponed    Test for Houdini decision procedure

 dafny0           Use    Dafny functionality tests

-dafny1		 Use	Various Dafny examples

+dafny1           Use    Various Dafny examples

 havoc0           Use    HAVOC-generated bpl files

 VSI-Benchmarks   Use    Solutions to Verified Software Initiative verification challenges

 vacid0           Use    Dafny attempts to VACID Edition 0 benchmarks

-livevars	 Use	STORM benchmarks for testing correctness of live variable analysis

-lazyinline	 Use	Lazy inlining benchmarks

-stratifiedinline	 Use	Stratified inlining benchmarks

+livevars         Use    STORM benchmarks for testing correctness of live variable analysis

+lazyinline       Use    Lazy inlining benchmarks

+stratifiedinline Use    Stratified inlining benchmarks

diff --git a/Test/codeexpr/Answer b/Test/codeexpr/Answer
new file mode 100644
index 00000000..55709034
--- /dev/null
+++ b/Test/codeexpr/Answer
@@ -0,0 +1,31 @@
+

+------------------------------ CodeExpr0.bpl ---------------------

+CodeExpr0.bpl(15,3): Error BP5001: This assertion might not hold.

+Execution trace:

+        CodeExpr0.bpl(15,3): anon0

+CodeExpr0.bpl(20,3): Error BP5001: This assertion might not hold.

+Execution trace:

+        CodeExpr0.bpl(20,3): anon0

+CodeExpr0.bpl(52,3): Error BP5001: This assertion might not hold.

+Execution trace:

+        CodeExpr0.bpl(52,3): anon0

+

+Boogie program verifier finished with 3 verified, 3 errors

+

+------------------------------ CodeExpr1.bpl ---------------------

+CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold at this return statement.

+CodeExpr1.bpl(40,3): Related location: This is the postcondition that might not hold.

+Execution trace:

+        CodeExpr1.bpl(42,3): start

+CodeExpr1.bpl(52,5): Error BP5001: This assertion might not hold.

+Execution trace:

+        CodeExpr1.bpl(49,3): start

+CodeExpr1.bpl(66,5): Error BP5001: This assertion might not hold.

+Execution trace:

+        CodeExpr1.bpl(57,3): start

+

+Boogie program verifier finished with 3 verified, 3 errors

+

+------------------------------ CodeExpr2.bpl ---------------------

+

+Boogie program verifier finished with 6 verified, 0 errors

diff --git a/Test/codeexpr/CodeExpr0.bpl b/Test/codeexpr/CodeExpr0.bpl
new file mode 100644
index 00000000..62a4225f
--- /dev/null
+++ b/Test/codeexpr/CodeExpr0.bpl
@@ -0,0 +1,53 @@
+procedure P()

+{

+  assert |{ A: return true; }|;

+}

+

+// ------------

+

+procedure Q()

+{

+  assert |{ var x: bool; A: x := true; return x; }|;

+}

+

+procedure R()

+{

+  assert |{ var x: bool; A: x := false; return x; }|;  // error

+}

+

+procedure S()

+{

+  assert |{ var x: bool; A: return x; }|;  // error

+}

+

+// ------------

+

+procedure T(x: int, y: int)

+  requires |{ var z: bool;

+              Start: goto A;

+              A: z := false; goto B, C;

+              B: assume 0 <= x; goto D;

+              C: assume x < 0; goto R;

+              D: goto E, F;

+              E: assume 0 <= y; z := true; goto R;

+              F: assume y < 0; goto R;

+              R: return z;

+           }|;

+{

+  assert 0 <= x + y;

+}

+

+procedure U(x: int, y: int)

+  requires |{ var z: bool;

+              Start: goto A;

+              A: z := false; goto B, C;

+              B: assume 0 <= x; goto D;

+              C: assume x < 0; goto R;

+              D: goto E, F;

+              E: assume 0 <= y; z := true; goto R;

+              F: assume y < 0; goto R;

+              R: return z;

+           }|;

+{

+  assert x <= y;  // error

+}

diff --git a/Test/codeexpr/CodeExpr1.bpl b/Test/codeexpr/CodeExpr1.bpl
new file mode 100644
index 00000000..3cc92333
--- /dev/null
+++ b/Test/codeexpr/CodeExpr1.bpl
@@ -0,0 +1,67 @@
+// ------ the good ------

+

+procedure F(x: int, y: int) returns (z: bool)

+  requires x < y;

+  ensures z == (x < 3);

+{

+  start:

+    z := |{ var a : bool, b : bool; B: a := x < 3; return a; }|;

+    return;

+}

+

+function r(int): bool;

+

+procedure F'(x: int, y: int) returns (z: bool)

+{

+  start:

+    assume x < y;

+    assume (forall t: int :: x < 3 + t ==> r(t));

+    assert r(y);

+}

+

+procedure F''(x: int, y: int) returns (z: bool)

+{

+  start:

+    assume x < y;

+    assume (forall t: int :: |{ var a: bool;

+                                Start:

+                                a := x < 3 + t;

+                                goto X, Y;

+                                X: assume a; return r(t);

+                                Y: assume !a; return true;

+                             }|);

+    assert r(y);

+}

+

+// ------ the bad ------

+

+procedure G(x: int, y: int) returns (z: bool)

+  requires x < y;

+  ensures z == (x < 3);

+{

+  start:

+    z := |{ var a : bool, b : bool; B: a := x < 3; return !a; }|;

+    return;  // error: postcondition violation

+}

+

+procedure G'(x: int, y: int) returns (z: bool)

+{

+  start:

+    assume x < y;

+    assume (forall t: int :: x + 3 < t ==> r(t));

+    assert r(y);  // error

+}

+

+procedure G''(x: int, y: int) returns (z: bool)

+{

+  start:

+    assume x < y;

+    assume (forall t: int :: |{ var a: bool;

+                                Start:

+                                a := x + 3 < t;

+                                goto X, Y;

+                                X: assume a; return r(t);

+                                Y: assume !a; return true;

+                             }|);

+    assert r(y);  // error

+}

diff --git a/Test/codeexpr/CodeExpr2.bpl b/Test/codeexpr/CodeExpr2.bpl
new file mode 100644
index 00000000..61758d5a
--- /dev/null
+++ b/Test/codeexpr/CodeExpr2.bpl
@@ -0,0 +1,50 @@
+type T;

+const zero: T;

+

+function IsProperIndex(i: int, size: int): bool;

+

+procedure P(a: [int]T, n: int)

+  requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);

+{

+  call Q(a, n);

+}

+

+procedure Q(a: [int]T, n: int)

+  requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);

+{

+  call P(a, n);

+}

+

+procedure A(a: [int]T, n: int)

+{

+  assert

+    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)

+    ==>

+    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);

+}

+

+procedure B(a: [int]T, n: int)

+{

+  assert

+    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)

+    ==>

+    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);

+}

+

+procedure C(a: [int]T, n: int)

+{

+  Start:

+    assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);

+    goto Next;

+  Next:

+    assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);

+}

+

+procedure D(a: [int]T, n: int)

+{

+  Start:

+    assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);

+    goto Next;

+  Next:

+    assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);

+}

diff --git a/Test/codeexpr/runtest.bat b/Test/codeexpr/runtest.bat
new file mode 100644
index 00000000..502081b1
--- /dev/null
+++ b/Test/codeexpr/runtest.bat
@@ -0,0 +1,10 @@
+@echo off

+

+set BOOGIEDIR=..\..\Binaries

+set BPLEXE=%BOOGIEDIR%\Boogie.exe

+

+for %%f in (CodeExpr0.bpl CodeExpr1.bpl CodeExpr2.bpl) do (

+  echo.

+  echo ------------------------------ %%f ---------------------

+  %BPLEXE% %* %%f

+)

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 2054998f..8452acb6 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -19,6 +19,11 @@ $pow2 -> {
   *8 -> *9

   else -> #unspecified

 }

+tickleBool -> {

+  *1 -> *0

+  *0 -> *0

+  else -> #unspecified

+}

 Ctor -> {

   *4 -> *8

   *5 -> *9

@@ -50,7 +55,7 @@ False : *1
 End of model.

 NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    NullInModel.bpl(2,3): anon0

+        NullInModel.bpl(2,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -71,6 +76,11 @@ $pow2 -> {
   *6 -> *7

   else -> #unspecified

 }

+tickleBool -> {

+  *1 -> *0

+  *0 -> *0

+  else -> #unspecified

+}

 Ctor -> {

   *4 -> *6

   *5 -> *7

@@ -94,7 +104,7 @@ False : *1
 End of model.

 IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    IntInModel.bpl(2,3): anon0

+        IntInModel.bpl(2,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -121,6 +131,11 @@ $pow2 -> {
   *13 -> *9

   else -> #unspecified

 }

+tickleBool -> {

+  *1 -> *0

+  *0 -> *0

+  else -> #unspecified

+}

 Ctor -> {

   *4 -> *13

   *5 -> *9

@@ -159,19 +174,19 @@ False : *1
 End of model.

 ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    ModelTest.bpl(3,5): anon0

+        ModelTest.bpl(3,5): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- InterpretedFunctionTests --------------------

 InterpretedFunctionTests.bpl(4,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    InterpretedFunctionTests.bpl(2,3): anon0

+        InterpretedFunctionTests.bpl(2,3): anon0

 InterpretedFunctionTests.bpl(10,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    InterpretedFunctionTests.bpl(8,3): anon0

+        InterpretedFunctionTests.bpl(8,3): anon0

 InterpretedFunctionTests.bpl(16,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    InterpretedFunctionTests.bpl(14,3): anon0

+        InterpretedFunctionTests.bpl(14,3): anon0

 

 Boogie program verifier finished with 0 verified, 3 errors