diff options
| author |  leino <unknown> | 2015-10-05 08:59:16 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-10-05 08:59:16 -0700 |
| commit | 27120ddc7adb3a0c789c1ee784d73a4be08de118 (patch) | |
| tree | 7f97308b82f9a829d4338e177e31713b8c10a803 /Test/dafny0/ResolutionErrors.dfy.expect | |
| parent | e07d86d6cc4423703dbfb479f09b44c80f877ef9 (diff) | |
Implemented resolution, verification, and (poorly performing) compilation of existential if guards.
Fixed bugs in ghost checks involving comprehensions and attributes.
Added SubstituteBoundedPool method.
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy.expect')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index be19eeac..b055184f 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -161,6 +161,11 @@ ResolutionErrors.dfy(1673,4): Error: 'decreases *' is not allowed on ghost loops ResolutionErrors.dfy(1677,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)
ResolutionErrors.dfy(1687,4): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(1691,29): 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)
+ResolutionErrors.dfy(1699,17): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1700,19): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1703,23): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1707,36): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1709,34): Error: the type of the bound variable 'u' could not be determined
ResolutionErrors.dfy(469,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -224,4 +229,4 @@ ResolutionErrors.dfy(1123,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1144,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1151,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1166,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-226 resolution/type errors detected in ResolutionErrors.dfy
+231 resolution/type errors detected in ResolutionErrors.dfy
|