diff options
Diffstat (limited to 'Test/test2')
-rw-r--r-- | Test/test2/Answer | 6 | ||||
-rw-r--r-- | Test/test2/Lambda.bpl | 8 | ||||
-rw-r--r-- | Test/test2/LambdaOldExpressions.bpl | 26 |
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];
+{
+}
|