diff options
| author |  Rustan Leino <unknown> | 2014-07-11 20:50:08 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-07-11 20:50:08 -0700 |
| commit | a8161c0e52d9c1743679091c36f64e925723d607 (patch) | |
| tree | 01d7b64cc2c85b81452e3aceba4318f6c1e68353 /Test/dafny0/ResolutionErrors.dfy.expect | |
| parent | 92cced2f7bde488e450fa12f7ef50d98f474ab61 (diff) | |
Added type synonyms. (No support yet for these in refinements.)
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy.expect')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 4075ff29..820465db 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -56,6 +56,16 @@ ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements ( ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(982,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3
ResolutionErrors.dfy(983,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C
+ResolutionErrors.dfy(994,7): Error: Duplicate name of top-level declaration: BadSyn2
+ResolutionErrors.dfy(991,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List
+ResolutionErrors.dfy(992,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)
+ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+ResolutionErrors.dfy(1000,7): Error: Cycle among type synonyms: A -> A
+ResolutionErrors.dfy(1003,7): Error: Cycle among type synonyms: A -> B -> A
+ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A
+ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A
+ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A
+ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x
ResolutionErrors.dfy(429,2): Error: More than one default constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts
@@ -84,6 +94,11 @@ ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can b ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
+ResolutionErrors.dfy(1031,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1034,20): Error: unresolved identifier: x
+ResolutionErrors.dfy(1037,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1039,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(1041,19): Error: unresolved identifier: x
ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)
@@ -147,4 +162,4 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real)
ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)
ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)
-149 resolution/type errors detected in ResolutionErrors.dfy
+164 resolution/type errors detected in ResolutionErrors.dfy
|