1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
LoopModifies.dfy(8,5): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(19,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(16,4): anon8_LoopHead
(0,0): anon8_LoopBody
LoopModifies.dfy(16,4): anon9_Else
LoopModifies.dfy(16,4): anon11_Else
LoopModifies.dfy(48,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(44,4): anon8_LoopHead
(0,0): anon8_LoopBody
LoopModifies.dfy(44,4): anon9_Else
LoopModifies.dfy(44,4): anon11_Else
LoopModifies.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(59,4): anon9_LoopHead
(0,0): anon9_LoopBody
LoopModifies.dfy(59,4): anon10_Else
LoopModifies.dfy(59,4): anon12_Else
LoopModifies.dfy(76,4): Error: loop modifies clause may violate context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(100,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(92,4): anon8_LoopHead
(0,0): anon8_LoopBody
LoopModifies.dfy(92,4): anon9_Else
LoopModifies.dfy(92,4): anon11_Else
LoopModifies.dfy(148,11): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(136,4): anon17_LoopHead
(0,0): anon17_LoopBody
LoopModifies.dfy(136,4): anon18_Else
LoopModifies.dfy(136,4): anon20_Else
LoopModifies.dfy(141,7): anon21_LoopHead
(0,0): anon21_LoopBody
LoopModifies.dfy(141,7): anon22_Else
LoopModifies.dfy(141,7): anon24_Else
LoopModifies.dfy(199,10): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(195,4): anon8_LoopHead
(0,0): anon8_LoopBody
LoopModifies.dfy(195,4): anon9_Else
LoopModifies.dfy(195,4): anon11_Else
LoopModifies.dfy(287,13): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(275,4): anon16_LoopHead
(0,0): anon16_LoopBody
LoopModifies.dfy(275,4): anon17_Else
LoopModifies.dfy(275,4): anon19_Else
LoopModifies.dfy(283,7): anon20_LoopHead
(0,0): anon20_LoopBody
LoopModifies.dfy(283,7): anon21_Else
LoopModifies.dfy(283,7): anon23_Else
Dafny program verifier finished with 23 verified, 9 errors
|
