From 2e03ed114503dfa16547c06766fa683c690f9052 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Thu, 18 Feb 2010 19:58:38 +0000
Subject: Implement if-then-else expression.

---
 Test/test1/Answer          | 4 ++++
 Test/test1/IfThenElse0.bpl | 8 ++++++++
 Test/test1/runtest.bat     | 1 +
 3 files changed, 13 insertions(+)
 create mode 100644 Test/test1/IfThenElse0.bpl

(limited to 'Test/test1')

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
-- 
cgit v1.2.3