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/Newtypes.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/Newtypes.dfy.expect')
| -rw-r--r-- | Test/dafny0/Newtypes.dfy.expect | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/Test/dafny0/Newtypes.dfy.expect b/Test/dafny0/Newtypes.dfy.expect index 2678e526..7af53142 100644 --- a/Test/dafny0/Newtypes.dfy.expect +++ b/Test/dafny0/Newtypes.dfy.expect @@ -19,5 +19,28 @@ Execution trace: Newtypes.dfy(104,16): Error: result of operation might violate newtype constraint
Execution trace:
(0,0): anon0
+Newtypes.dfy(177,14): Error: result of operation might violate newtype constraint
+Execution trace:
+ (0,0): anon0
+Newtypes.dfy(193,64): Error: index 0 out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon32_Then
+ (0,0): anon33_Then
+ (0,0): anon16
+Newtypes.dfy(194,67): Error: index 1 out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon34_Then
+ (0,0): anon35_Then
+ (0,0): anon19
+Newtypes.dfy(222,16): Error: new number of occurrences might be negative
+Execution trace:
+ (0,0): anon0
+ (0,0): anon6_Then
+Newtypes.dfy(225,40): Error: result of operation might violate newtype constraint
+Execution trace:
+ (0,0): anon0
+ (0,0): anon8_Then
-Dafny program verifier finished with 30 verified, 6 errors
+Dafny program verifier finished with 35 verified, 11 errors
|