diff options
Diffstat (limited to 'Test/triggers/loop-detection-is-not-too-strict.dfy')
| -rw-r--r-- | Test/triggers/loop-detection-is-not-too-strict.dfy | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy index a5a30c81..81f764ad 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy @@ -7,8 +7,9 @@ // equal to that trigger, as long as the only differences are variable
predicate P(x: int, y: int)
+predicate Q(x: int)
-method Test() {
+method Test(z: int) {
// P(x, y) and P(y, x) might look like they would cause a loop. Since they
// only differ by their variables, though, they won't raise flags.
assume forall x: int, y: int :: P(x, y) == P(y, x);
@@ -18,4 +19,22 @@ method Test() { // Contrast with the following:
assume forall x: int, y: int :: P(x, y) == P(x, y+1);
+
+ // The following examples were made legal after an exchange where Chris
+ // pointed examples in the IronClad sources where things like this were
+ // incorrectly flagged.
+ assert forall x :: true || Q(x) || Q(0);
+ assert forall x :: true || Q(x) || Q(z);
+ assert forall x :: true || P(x, 1) || P(x, z);
+
+ // Support for the following was added following a discussion with Rustan; in
+ // the second one the expression `if z > 1 then z else 3 * z + 1` is not
+ // directly a constant expression, but it does not involve x, so it's ok:
+ assert forall x :: true || Q(x) || Q(0+1);
+ assert forall x :: true || Q(x) || Q(if z > 1 then z else 3 * z + 1);
+ // Sanity check:
+ assert forall x :: true || Q(x) || Q(if z > 1 then x else 3 * z + 1);
+
+ // WISH: It might also be good to zeta-reduce before loop detection.
+ assert forall x :: true || Q(x) || (var xx := x+1; Q(xx));
}
|