Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda expressions; they might not yet fully work for polymorphic maps.

3 files changed, 52 insertions, 1 deletions

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