From 84b52a48efda3e9658b772dbc02d34a6f6c9d16b Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 21 Aug 2015 19:09:37 -0700 Subject: Adjust WF checks to use unsplit quantifiers. The logic about split quantifiers is that Boogie (and z3) should never realize that there was an unsplit quantifier. The WF check code does not produce a quantifier, at least in it's checking part; thus, it should use original quantifier. This fixes a problem in VerifyThis2015/Problem2.dfy with a null check, and a problem spotted by Chris, made into a test case saved in triggers/wf-checks-use-the-original-quantifier.dfy. The issue boiled down to being able to verify (forall x :: x != null && x.a == 0). Of course, the assumption that WF checks produce for a quantifier is a quantifier, so it uses the split expression. --- .../wf-checks-use-the-original-quantifier.dfy | 28 ++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 Test/triggers/wf-checks-use-the-original-quantifier.dfy (limited to 'Test/triggers/wf-checks-use-the-original-quantifier.dfy') diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy b/Test/triggers/wf-checks-use-the-original-quantifier.dfy new file mode 100644 index 00000000..a1a2bd90 --- /dev/null +++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy @@ -0,0 +1,28 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This test checks that typical expressions requiring WF checks do not suddenly +// loose expressivity due to quantifier splitting. Without special care, the +// expression (forall x :: x != null && x.a == 0) could fail to verify. + +// The logic about split quantifiers is that Boogie (and z3) should never realize +// that there was an unsplit quantifier. The WF check code does not produce a +// quantifier, at least in it's checking part; thus, it should use original +// quantifier. This fixes a problem in VerifyThis2015/Problem2.dfy with a null +// check, and a problem spotted by Chris, made into a test case saved in +// triggers/wf-checks-use-the-original-quantifier.dfy. + +// Of course, the assumption that WF checks produce for a quantifier is a +// quantifier, so the assumption part that comes after the WF check does use the +// split expression. + +// This test case is inspired by the example that Chris gave. + +predicate P(b: nat) +function f(a: int): int +class C { var x: int; } + +method M(s: set) + requires forall n: nat :: 0 <= f(n) && P(f(n)) + requires forall c, c' | c in s && c' in s :: c != null && c'!= null && c.x == c'.x { +} -- cgit v1.2.3