diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-14 19:46:49 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-14 19:46:49 -0700 |
| commit | dc721907edfd78d6e12ed4155b14c960416791c4 (patch) | |
| tree | ab98f3d91e3671fcb0b3245b3fe99ba7f6383f56 /Test | |
| parent | aa2bfc0930e932be72cfd2d796352a0aa4182477 (diff) | |
Fix broken interaction between triggers and inlining of function calls
The problem was that inlining would replace formals with arguments in triggers
as well, causing invalid expressions ("trigger killers") to pop up in triggers
after inlining.
This fix disables inlining if it can't be determined that it won't lead to an
invalid trigger. If that procedure is incomplete, then that's only by a narrow
margin, as the checks actually ensure that the formals that are getting trigger
killers are indeed used in triggers.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/new-tests/trigger-in-predicate.dfy | 15 | ||||
| -rw-r--r-- | Test/new-tests/trigger-in-predicate.dfy.expect | 4 |
2 files changed, 19 insertions, 0 deletions
diff --git a/Test/new-tests/trigger-in-predicate.dfy b/Test/new-tests/trigger-in-predicate.dfy new file mode 100644 index 00000000..880d3d1d --- /dev/null +++ b/Test/new-tests/trigger-in-predicate.dfy @@ -0,0 +1,15 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate A(x: bool, y: bool) { x }
+
+predicate B(x: bool, z: bool) { forall y {:trigger A(x, y) } :: A(x, y) && z }
+
+// Inlining is disabled here to prevent pollution of the trigger in B
+method C() requires B(true || false, true) {}
+
+// Inlining should work fine here
+method C'() requires B(true, true) {}
+
+// Inlining should work fine here
+method C''() requires B(true, true && false) {}
diff --git a/Test/new-tests/trigger-in-predicate.dfy.expect b/Test/new-tests/trigger-in-predicate.dfy.expect new file mode 100644 index 00000000..211bc9a2 --- /dev/null +++ b/Test/new-tests/trigger-in-predicate.dfy.expect @@ -0,0 +1,4 @@ +c:/MSR/dafny-triggers/Test/new-tests/trigger-in-predicate.dfy(9,21): Info: This call cannot be safely inlined.
+c:/MSR/dafny-triggers/Test/new-tests/trigger-in-predicate.dfy(9,21): Info: This call cannot be safely inlined.
+
+Dafny program verifier finished with 8 verified, 0 errors
|