diff options
| author |  leino <unknown> | 2014-08-26 11:29:55 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-26 11:29:55 -0700 |
| commit | b160a16857b62e8ea47774939afde8f51454941f (patch) | |
| tree | 7a30fa705759d1e2f7faad5b18c652b5d06fd7e8 /Test/dafny0/NewtypesResolution.dfy.expect | |
| parent | cf01d66976ffd99f423b93949d0f80bba03fe5d7 (diff) | |
Renamed some test files.
Diffstat (limited to 'Test/dafny0/NewtypesResolution.dfy.expect')
| -rw-r--r-- | Test/dafny0/NewtypesResolution.dfy.expect | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/Test/dafny0/NewtypesResolution.dfy.expect b/Test/dafny0/NewtypesResolution.dfy.expect new file mode 100644 index 00000000..091ca523 --- /dev/null +++ b/Test/dafny0/NewtypesResolution.dfy.expect @@ -0,0 +1,25 @@ +DerivedTypesResolution.dfy(5,7): Error: Cycle among redirecting types (newtypes, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym
+DerivedTypesResolution.dfy(12,10): Error: newtypes must be based on some numeric type (got List<int>)
+DerivedTypesResolution.dfy(38,9): Error: arguments must have the same type (got posReal and real)
+DerivedTypesResolution.dfy(44,9): Error: arguments must have the same type (got int32 and int)
+DerivedTypesResolution.dfy(50,13): Error: arguments must have the same type (got posReal and int32)
+DerivedTypesResolution.dfy(51,13): Error: arguments to <= must have the same type (got posReal and int32)
+DerivedTypesResolution.dfy(52,13): Error: arguments to < must have the same type (got int32 and int)
+DerivedTypesResolution.dfy(53,13): Error: arguments to > must have the same type (got posReal and real)
+DerivedTypesResolution.dfy(57,13): Error: first argument to % must be of type int (instead got posReal)
+DerivedTypesResolution.dfy(57,25): Error: first argument to % must be of type int (instead got real)
+DerivedTypesResolution.dfy(75,8): Error: newtype constraint must be of type bool (instead got SmallInt)
+DerivedTypesResolution.dfy(77,10): Error: unresolved identifier: a
+DerivedTypesResolution.dfy(91,31): Error: old expressions are not allowed in this context
+DerivedTypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N
+DerivedTypesResolution.dfy(105,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle
+DerivedTypesResolution.dfy(114,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle
+DerivedTypesResolution.dfy(120,21): Error: name of type ('N9') is used as a variable
+DerivedTypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int)
+DerivedTypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int)
+DerivedTypesResolution.dfy(156,9): Error: name of type ('B') is used as a variable
+DerivedTypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variable
+DerivedTypesResolution.dfy(162,8): Error: member U does not exist in class Klass
+DerivedTypesResolution.dfy(162,4): Error: expected method call, found expression
+DerivedTypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)
+24 resolution/type errors detected in DerivedTypesResolution.dfy
|