Implement if-then-else expression.

6 files changed, 59 insertions, 1 deletions

diff --git a/Test/test1/Answer b/Test/test1/Answer
index b0f4aac3..10ad5494 100644
--- a/Test/test1/Answer
+++ b/Test/test1/Answer
@@ -135,3 +135,7 @@ FunBody.bpl(6,45): Error: function body with invalid type: bool (expected: int)
 FunBody.bpl(8,61): Error: function body with invalid type: int (expected: alpha)

 FunBody.bpl(10,58): Error: function body with invalid type: int (expected: alpha)

 3 type checking errors detected in FunBody.bpl

+IfThenElse0.bpl(5,7): Error: the first argument to if-then-else should be bool, not int

+IfThenElse0.bpl(6,7): Error: branches of if-then-else have incompatible types bool and int

+IfThenElse0.bpl(7,2): Error: mismatched types in assignment command (cannot assign int to bool)

+3 type checking errors detected in IfThenElse0.bpl

diff --git a/Test/test1/IfThenElse0.bpl b/Test/test1/IfThenElse0.bpl
new file mode 100644
index 00000000..c26461b1
--- /dev/null
+++ b/Test/test1/IfThenElse0.bpl
@@ -0,0 +1,8 @@
+procedure foo()
+{
+  var b:bool, i:int;
+
+  b := if i then b else b;
+  b := if b then b else i;
+  b := if b then i else i;
+}
diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat
index c6881263..dda3a0af 100644
--- a/Test/test1/runtest.bat
+++ b/Test/test1/runtest.bat
@@ -17,3 +17,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe
 %BGEXE% %* /noVerify Orderings.bpl

 %BGEXE% %* /noVerify EmptyCallArgs.bpl

 %BGEXE% %* /noVerify FunBody.bpl

+%BGEXE% %* /noVerify IfThenElse0.bpl

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 1e5a0d5f..230a8861 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -323,6 +323,16 @@ Execution trace:
     Implies.bpl(11,3): anon0

 

 Boogie program verifier finished with 0 verified, 2 errors

+

+-------------------- IfThenElse1.bpl --------------------

+IfThenElse1.bpl(26,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    IfThenElse1.bpl(26,3): anon0

+IfThenElse1.bpl(33,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    IfThenElse1.bpl(33,3): anon0

+

+Boogie program verifier finished with 2 verified, 2 errors

 -------------------- sk_hack.bpl --------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/test2/IfThenElse1.bpl b/Test/test2/IfThenElse1.bpl
new file mode 100644
index 00000000..8a867f50
--- /dev/null
+++ b/Test/test2/IfThenElse1.bpl
@@ -0,0 +1,34 @@
+type t1;
+
+procedure ok()
+{
+  var b:bool, x:int, y:int;
+
+  assert x == if b then x else x;
+  assert x == if true then x else y;
+}
+
+procedure ok2()
+{
+  var x:int, y:int;
+  var a:t1, b:t1, c:t1;
+
+  c := if x > y then a else b;
+  assert c == a || c == b;
+  assume x > y;
+  assert c == a;
+}
+
+procedure fail1()
+{
+  var b:bool, x:int, y:int;
+
+  assert x == if b then x else y;
+}
+
+procedure fail2()
+{
+  var b:bool, x:int, y:int;
+
+  assert x == if false then x else y;
+}
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index 5f48a799..ab9ec103 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -10,7 +10,8 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
             CutBackEdge.bpl False.bpl LoopInvAssume.bpl

             strings-no-where.bpl strings-where.bpl

             Structured.bpl Where.bpl UpdateExpr.bpl

-            NeverPattern.bpl NullaryMaps.bpl Implies.bpl) do (

+            NeverPattern.bpl NullaryMaps.bpl Implies.bpl

+	    IfThenElse1.bpl) do (

   echo.

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

   %BGEXE% %* /noinfer %%f