Changed all lambda-expression rewriting to be done as a pre-processing step before real verification.

Fixed treatment of lambda-expression attributes.

3 files changed, 35 insertions, 5 deletions

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 609cf1ed..ecec6339 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -369,7 +369,7 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
 Execution trace:

     Lambda.bpl(36,5): anon0

 

-Boogie program verifier finished with 5 verified, 2 errors

+Boogie program verifier finished with 6 verified, 2 errors

 

 -------------------- LambdaPoly.bpl --------------------

 LambdaPoly.bpl(28,5): Error BP5001: This assertion might not hold.

@@ -393,7 +393,7 @@ LambdaOldExpressions.bpl(21,3): Related location: This is the postcondition that
 Execution trace:

     LambdaOldExpressions.bpl(25,7): anon0

 

-Boogie program verifier finished with 2 verified, 1 error

+Boogie program verifier finished with 4 verified, 1 error

 

 -------------------- SelectiveChecking.bpl --------------------

 SelectiveChecking.bpl(17,3): Error BP5001: This assertion might not hold.

@@ -453,7 +453,7 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
 Execution trace:

     Lambda.bpl(36,5): anon0

 

-Boogie program verifier finished with 5 verified, 2 errors

+Boogie program verifier finished with 6 verified, 2 errors

 

 -------------------- TypeEncodingM.bpl /typeEncoding:m --------------------

 TypeEncodingM.bpl(24,3): Error BP5001: This assertion might not hold.

diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl
index 477d0f36..68c83d43 100644
--- a/Test/test2/Lambda.bpl
+++ b/Test/test2/Lambda.bpl
@@ -63,3 +63,11 @@ procedure nestedLambda()
   a := (lambda x: int :: (lambda y: int :: x+y));
 }
 
+// The following tests that the lambda in the desugaring of the
+// call command gets replaced.
+procedure P();
+  ensures (lambda y: int :: y == y)[15];
+procedure Q()
+{
+  call P();
+}
diff --git a/Test/test2/LambdaOldExpressions.bpl b/Test/test2/LambdaOldExpressions.bpl
index c26b0198..9f17245f 100644
--- a/Test/test2/LambdaOldExpressions.bpl
+++ b/Test/test2/LambdaOldExpressions.bpl
@@ -4,8 +4,8 @@ var b: bool;
 procedure p0();

   requires b;

   modifies b;

-  ensures (lambda x: bool :: old(b))[true];

-  ensures !(lambda x: bool :: b)[true];

+  ensures (lambda x: bool :: {:MyAttr "put an attr here", !b} old(b))[true];

+  ensures !(lambda x: bool :: {:AnotherAttr "yes, why not", b} {:ABC b, b, old(b)} b)[true];

 

 implementation p0()

 {

@@ -37,3 +37,25 @@ implementation p2()
     b := !b;

     assert (lambda x: bool :: old(b) != b)[true];

 }

+

+

+procedure p3();

+  requires b;

+  modifies b;

+  ensures (lambda x: int :: old(old(b)) != b)[15];

+

+implementation p3()

+{

+    b := !b;

+    assert (lambda x: int :: old(old(b)) != b)[15];

+}

+

+// Note that variables (inside and outside old expressions) mentioned

+// in attributes (even if they are not mentioned in the body of the

+// lambda) are also picked up by the auto-generated lambda functions,

+// so that the attributes can be copied to the function and axiom.

+var h: int;

+procedure TestAttributeParameters()

+  ensures (lambda x: int :: {:MyAttribute old(h), h} x < 100)[23];

+{

+}