diff options
| author |  leino <unknown> | 2015-09-28 13:16:15 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-28 13:16:15 -0700 |
| commit | 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 (patch) | |
| tree | cb89d6ef66c96bfa171f954898548f295a3cabc0 /Test/dafny4/set-compr.dfy.expect | |
| parent | ebaaa36321463925dc9030455e87ae17732b2353 (diff) | |
Changed computation of ghosts until pass 2 of resolution.
Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.
Diffstat (limited to 'Test/dafny4/set-compr.dfy.expect')
| -rw-r--r-- | Test/dafny4/set-compr.dfy.expect | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect index b31c6ac0..615ee2bc 100644 --- a/Test/dafny4/set-compr.dfy.expect +++ b/Test/dafny4/set-compr.dfy.expect @@ -1,3 +1,3 @@ -set-compr.dfy(25,7): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-set-compr.dfy(51,13): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+set-compr.dfy(25,7): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
+set-compr.dfy(51,13): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
2 resolution/type errors detected in set-compr.dfy
|