diff options
Diffstat (limited to 'Test/dafny0/Array.dfy.expect')
| -rw-r--r-- | Test/dafny0/Array.dfy.expect | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect index ff05137b..59dcb4bf 100644 --- a/Test/dafny0/Array.dfy.expect +++ b/Test/dafny0/Array.dfy.expect @@ -48,6 +48,7 @@ Execution trace: (0,0): anon11_Then
(0,0): anon12_Then
(0,0): anon13_Then
+ (0,0): anon9
Array.dfy(122,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
(0,0): anon0
@@ -55,6 +56,7 @@ Execution trace: (0,0): anon11_Then
(0,0): anon12_Then
(0,0): anon13_Else
+ (0,0): anon9
Array.dfy(123,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
(0,0): anon0
@@ -62,6 +64,7 @@ Execution trace: (0,0): anon11_Then
(0,0): anon12_Then
(0,0): anon13_Else
+ (0,0): anon9
Array.dfy(124,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
(0,0): anon0
@@ -69,18 +72,21 @@ Execution trace: (0,0): anon11_Then
(0,0): anon12_Then
(0,0): anon13_Else
+ (0,0): anon9
Array.dfy(163,6): Error: insufficient reads clause to read array element
Execution trace:
(0,0): anon0
(0,0): anon8_Else
(0,0): anon9_Then
(0,0): anon10_Then
+ (0,0): anon7
Array.dfy(171,6): Error: insufficient reads clause to read array element
Execution trace:
(0,0): anon0
(0,0): anon8_Else
(0,0): anon9_Then
(0,0): anon10_Then
+ (0,0): anon7
Array.dfy(187,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
|