diff options
| author |  wuestholz <unknown> | 2011-12-02 10:58:47 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2011-12-02 10:58:47 +0100 |
| commit | a16ac98f4aa7657d999753e299e32613e10f1c5d (patch) | |
| tree | daf540ec9cca24386a3c3dc8131ddb10dd4236ff /Test/test2 | |
| parent | 34112b0b3da6642b5b18ce2dd53d6b6d57cc214f (diff) | |
Boogie: Fixed a crash due to old expressions in lambda expressions that were not replaced after lambda expansion.
(reported by Florian Egli)
Diffstat (limited to 'Test/test2')
| -rw-r--r-- | Test/test2/LambdaOldExpressions.bpl | 39 | ||||
| -rw-r--r-- | Test/test2/runtest.bat | 3 |
2 files changed, 41 insertions, 1 deletions
diff --git a/Test/test2/LambdaOldExpressions.bpl b/Test/test2/LambdaOldExpressions.bpl new file mode 100644 index 00000000..c26b0198 --- /dev/null +++ b/Test/test2/LambdaOldExpressions.bpl @@ -0,0 +1,39 @@ +var b: bool;
+
+
+procedure p0();
+ requires b;
+ modifies b;
+ ensures (lambda x: bool :: old(b))[true];
+ ensures !(lambda x: bool :: b)[true];
+
+implementation p0()
+{
+ b := !b;
+ assert (lambda x: bool :: old(b))[true];
+ assert !(lambda x: bool :: b)[true];
+}
+
+
+procedure p1();
+ requires !b;
+ modifies b;
+ ensures (lambda x: bool :: old(b))[true]; // error
+
+implementation p1()
+{
+ b := !b;
+ assert !(lambda x: bool :: old(b))[true];
+}
+
+
+procedure p2();
+ requires b;
+ modifies b;
+ ensures (lambda x: bool :: old(b) != b)[true];
+
+implementation p2()
+{
+ b := !b;
+ assert (lambda x: bool :: old(b) != b)[true];
+}
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat index 8ce2f66e..f32bf844 100644 --- a/Test/test2/runtest.bat +++ b/Test/test2/runtest.bat @@ -11,7 +11,8 @@ 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 Lambda.bpl LambdaPoly.bpl SelectiveChecking.bpl FreeCall.bpl) do (
+ IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl LambdaOldExpressions.bpl
+ SelectiveChecking.bpl FreeCall.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /noinfer %%f
|