diff options
| author |  leino <unknown> | 2014-08-20 20:26:08 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-20 20:26:08 -0700 |
| commit | a570ecd2d288f67a9e56faf4421a447d06b21d36 (patch) | |
| tree | d333228b3ece459feb1ef207fb7628dce16e38bd /Test/dafny0/ResolutionErrors.dfy.expect | |
| parent | 61d55705cdf6a710f1a21ddb2ae2caaa314ca7f6 (diff) | |
| parent | bc5ba2bcd7fb7de092898100e08edecf9f0a00e1 (diff) | |
Merge
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy.expect')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index b6ebe5dc..4827dc07 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -134,7 +134,7 @@ ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label ResolutionErrors.dfy(263,2): Error: duplicate label
ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(292,4): Error: a constructor is only allowed to be called when an object is being allocated
+ResolutionErrors.dfy(292,4): Error: a constructor is allowed to be called only when an object is being allocated
ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List)
ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int)
ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int)
@@ -176,4 +176,6 @@ ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)
ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)
-178 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(1129,2): 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(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+180 resolution/type errors detected in ResolutionErrors.dfy
|