diff options
| author |  leino <unknown> | 2014-10-06 18:56:48 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-06 18:56:48 -0700 |
| commit | 8dcec3ddb5269c5e7195a8072d13e8e547b14323 (patch) | |
| tree | 32e6519bbf11e6301bdd763838d54e196ca5f7f6 /Test/dafny0/NewtypesResolution.dfy.expect | |
| parent | 51d67784f9b26a670f6a9f908f7dc1e474b6850c (diff) | |
Allow any integer-based type, not just 'int', in the following places:
* array indices (any dimension)
* array lengths (with new, any dimension)
* sequence indicies
* subsequence bounds (like sq[lo..hi])
* the new multiplicity in multiset update (m[t := multiplicity])
* subarray-to-sequence bounds (like a[lo..hi])
Note that for an array 'a', 'a.Length' is always an integer, so a comparison 'i < a.Length' still requires 'i' to be an integer, not any integer-based value. Same for '|sq|' for a sequence 'sq'.
Diffstat (limited to 'Test/dafny0/NewtypesResolution.dfy.expect')
| -rw-r--r-- | Test/dafny0/NewtypesResolution.dfy.expect | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/Test/dafny0/NewtypesResolution.dfy.expect b/Test/dafny0/NewtypesResolution.dfy.expect index 81c43d35..bb1624f9 100644 --- a/Test/dafny0/NewtypesResolution.dfy.expect +++ b/Test/dafny0/NewtypesResolution.dfy.expect @@ -22,4 +22,13 @@ NewtypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variabl NewtypesResolution.dfy(162,8): Error: member U does not exist in class Klass
NewtypesResolution.dfy(162,4): Error: expected method call, found expression
NewtypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)
-24 resolution/type errors detected in NewtypesResolution.dfy
+NewtypesResolution.dfy(219,11): Error: new must use an integer-based expression for the array size (got real for index 2)
+NewtypesResolution.dfy(221,13): Error: arguments to < must have the same type (got Even and nat)
+NewtypesResolution.dfy(223,13): Error: arguments to < must have the same type (got Even and int)
+NewtypesResolution.dfy(227,13): Error: arguments to < must have the same type (got Even and int)
+NewtypesResolution.dfy(229,13): Error: arguments to < must have the same type (got Even and int)
+NewtypesResolution.dfy(230,13): Error: arguments to < must have the same type (got Even and int)
+NewtypesResolution.dfy(238,13): Error: arguments to < must have the same type (got Even and int)
+NewtypesResolution.dfy(240,13): Error: arguments to <= must have the same type (got Even and int)
+NewtypesResolution.dfy(249,17): Error: multiset update requires integer-based numeric value (got real)
+33 resolution/type errors detected in NewtypesResolution.dfy
|