diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-27 14:31:53 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-27 14:31:53 -0700 |
| commit | b541877f2a5cbc59c5d923cd84e59dbe6e12c02d (patch) | |
| tree | 63803f6dd65120a5644ea9c2ed81a8ce2bcabbb8 /Source | |
| parent | a8bdd2aa3fcbff708b233ee321b13a17f232ce19 (diff) | |
Dafny: fixed unsoundness having to do with a function depending on the allocation state
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 233f5415..daeef80c 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2934,7 +2934,21 @@ namespace Microsoft.Dafny { var missingBounds = new List<BoundVar>();
e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, missingBounds);
if (missingBounds.Count != 0) {
- e.MissingBounds = missingBounds;
+ // Report errors here about quantifications that depend on the allocation state.
+ var mb = missingBounds;
+ if (currentFunction != null) {
+ mb = new List<BoundVar>(); // (who cares if we allocate another array; this happens only in the case of a resolution error anyhow)
+ foreach (var bv in missingBounds) {
+ if (bv.Type.IsRefType) {
+ Error(expr, "a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{0}'", bv.Name);
+ } else {
+ mb.Add(bv);
+ }
+ }
+ }
+ if (mb.Count != 0) {
+ e.MissingBounds = mb;
+ }
}
}
@@ -3501,7 +3515,7 @@ namespace Microsoft.Dafny { // easy
bounds.Add(new QuantifierExpr.BoolBoundedPool());
} else {
- // Go through the conjuncts of the range expression look for bounds.
+ // Go through the conjuncts of the range expression to look for bounds.
Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;
Expression upperBound = null;
foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {
|