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

Fixed treatment of lambda-expression attributes.

1 files changed, 24 insertions, 2 deletions

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];

+{

+}