diff options
| author |  Rustan Leino <unknown> | 2015-07-31 16:58:36 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-07-31 16:58:36 -0700 |
| commit | d023b0e19f7bf886801a3a059511b8449d8ab223 (patch) | |
| tree | 1517417d51d4ef5d3190f13ff6b3dc7b82347429 /Test/dafny0/ResolutionErrors.dfy.expect | |
| parent | 8c1a52e085aed20f62a5d24fb2af9bbd5cb3e469 (diff) | |
Bug fix: check that assign-such-that constraint is of type boolean
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy.expect')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 481b47e0..b5c93ac1 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -104,6 +104,10 @@ ResolutionErrors.dfy(1371,16): Error: name of module (Y) is used as a variable ResolutionErrors.dfy(1371,13): Error: arguments must have the same type (got int and #module)
ResolutionErrors.dfy(1372,4): Error: name of type (X) is used as a variable
ResolutionErrors.dfy(1373,4): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1382,11): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1383,9): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1384,13): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1387,15): Error: type of RHS of let-such-that expression must be boolean (got int)
ResolutionErrors.dfy(432,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')
@@ -196,4 +200,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1134,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(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-198 resolution/type errors detected in ResolutionErrors.dfy
+202 resolution/type errors detected in ResolutionErrors.dfy
|