From 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 28 Sep 2015 13:16:15 -0700 Subject: 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. --- Test/dafny0/DiscoverBounds.dfy.expect | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Test/dafny0/DiscoverBounds.dfy.expect') diff --git a/Test/dafny0/DiscoverBounds.dfy.expect b/Test/dafny0/DiscoverBounds.dfy.expect index ee816683..34003053 100644 --- a/Test/dafny0/DiscoverBounds.dfy.expect +++ b/Test/dafny0/DiscoverBounds.dfy.expect @@ -1,4 +1,4 @@ -DiscoverBounds.dfy(36,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'' -DiscoverBounds.dfy(39,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r' -DiscoverBounds.dfy(40,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r'' +DiscoverBounds.dfy(36,7): Error: quantifiers 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'' +DiscoverBounds.dfy(39,7): Error: quantifiers 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 'r' +DiscoverBounds.dfy(40,7): Error: quantifiers 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 'r'' 3 resolution/type errors detected in DiscoverBounds.dfy -- cgit v1.2.3