diff options
| author |  rustanleino <unknown> | 2011-03-26 04:06:37 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-26 04:06:37 +0000 |
| commit | bd9003ec46d72f74c3284a63713336da630769ff (patch) | |
| tree | 9ef94aac6ff8ec9982960dec816b778f78c3d63a /Test/dafny0/Answer | |
| parent | dceef1d90bfc91be2ab309107d3947ce1b3667eb (diff) | |
Dafny: improved and corrected physical/ghost distinction
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index b1e12099..08570842 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -407,7 +407,8 @@ NonGhostQuantifiers.dfy(71,5): Error: quantifiers in non-ghost contexts must be NonGhostQuantifiers.dfy(86,5): 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 'j'
NonGhostQuantifiers.dfy(94,10): 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 'y'
NonGhostQuantifiers.dfy(103,8): 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 'x'
-7 resolution/type errors detected in NonGhostQuantifiers.dfy
+NonGhostQuantifiers.dfy(120,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+8 resolution/type errors detected in NonGhostQuantifiers.dfy
-------------------- Modules0.dfy --------------------
Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
|