From 1127ea8d8037278415fa5cb2d8917d972b122983 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Fri, 19 Feb 2010 21:52:12 +0000
Subject: Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda
 expressions; they might not yet fully work for polymorphic maps.

---
 Test/test2/Answer      | 10 ++++++++++
 Test/test2/Lambda.bpl  | 41 +++++++++++++++++++++++++++++++++++++++++
 Test/test2/runtest.bat |  2 +-
 3 files changed, 52 insertions(+), 1 deletion(-)
 create mode 100644 Test/test2/Lambda.bpl

(limited to 'Test/test2')

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 230a8861..60d76af1 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -333,6 +333,16 @@ Execution trace:
     IfThenElse1.bpl(33,3): anon0
 
 Boogie program verifier finished with 2 verified, 2 errors
+
+-------------------- Lambda.bpl --------------------
+Lambda.bpl(37,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    Lambda.bpl(36,5): anon0
+Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    Lambda.bpl(36,5): anon0
+
+Boogie program verifier finished with 3 verified, 2 errors
 -------------------- sk_hack.bpl --------------------
 
 Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl
new file mode 100644
index 00000000..48610ff1
--- /dev/null
+++ b/Test/test2/Lambda.bpl
@@ -0,0 +1,41 @@
+procedure foo()
+{
+  var a: [int]int;
+  var c:int,b:bool;
+  a := (lambda y:int :: if b then y + c else 7);
+  assume b;
+  assert a[3] == c+3;
+}
+
+procedure bar()
+{
+  assert (lambda x:int :: x > 0)[10];
+  
+}
+
+type t1;
+
+procedure baz()
+{
+  var m:[int,t1]int;
+  var t:t1, t2:t1;
+
+  m := (lambda i:int, tt:t1 :: if tt == t then i else 12);
+  assert m[1,t] == 1;
+  assert t == t2 || m[1,t2] == 12;
+  assert  m[12,t2] == 12;
+  
+}
+
+
+procedure fail()
+{
+  var m:[int,t1]int;
+  var t:t1, t2:t1;
+
+  m := (lambda i:int, tt:t1 :: if tt == t then i else 12);
+  assert m[1,t2] == 12;
+  assert m[1,t] == 2;
+}
+
+
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index ab9ec103..ea4376b6 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -11,7 +11,7 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
             strings-no-where.bpl strings-where.bpl
             Structured.bpl Where.bpl UpdateExpr.bpl
             NeverPattern.bpl NullaryMaps.bpl Implies.bpl
-	    IfThenElse1.bpl) do (
+	    IfThenElse1.bpl Lambda.bpl) do (
   echo.
   echo -------------------- %%f --------------------
   %BGEXE% %* /noinfer %%f
-- 
cgit v1.2.3