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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
Definedness.dfy(11,7): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon3_Else
Definedness.dfy(18,16): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(27,16): Error: target object may be null
Execution trace:
(0,0): anon0
Definedness.dfy(28,21): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon3_Then
Definedness.dfy(29,17): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(36,16): Error: target object may be null
Execution trace:
(0,0): anon0
Definedness.dfy(45,16): Error: target object may be null
Execution trace:
(0,0): anon0
Definedness.dfy(53,18): Error: target object may be null
Execution trace:
(0,0): anon0
Definedness.dfy(54,3): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(53,22): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
Definedness.dfy(60,18): Error: target object may be null
Execution trace:
(0,0): anon0
Definedness.dfy(61,3): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(60,22): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
Definedness.dfy(68,3): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(67,22): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
Definedness.dfy(88,7): Error: target object may be null
Execution trace:
(0,0): anon0
Definedness.dfy(89,5): Error: possible violation of function precondition
Definedness.dfy(79,16): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(89,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
Definedness.dfy(89,10): Error: target object may be null
Execution trace:
(0,0): anon0
Definedness.dfy(90,10): Error: possible violation of function precondition
Definedness.dfy(79,16): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(95,14): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(95,23): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(96,15): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(101,12): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(108,15): Error: possible division by zero
Execution trace:
Definedness.dfy(108,5): anon7_LoopHead
(0,0): anon7_LoopBody
Definedness.dfy(108,5): anon8_Else
Definedness.dfy(117,23): Error: possible violation of function precondition
Definedness.dfy(79,16): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(116,5): anon12_LoopHead
(0,0): anon12_LoopBody
(0,0): anon13_Then
Definedness.dfy(123,17): Error: possible violation of function precondition
Definedness.dfy(79,16): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(116,5): anon12_LoopHead
(0,0): anon12_LoopBody
Definedness.dfy(116,5): anon13_Else
(0,0): anon14_Then
Definedness.dfy(122,5): anon15_LoopHead
(0,0): anon15_LoopBody
(0,0): anon16_Then
Definedness.dfy(133,17): Error: possible violation of function precondition
Definedness.dfy(79,16): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(132,5): anon6_LoopHead
(0,0): anon6_LoopBody
(0,0): anon7_Then
Definedness.dfy(133,22): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
Definedness.dfy(134,17): Error: possible violation of function precondition
Definedness.dfy(79,16): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(132,5): anon6_LoopHead
(0,0): anon6_LoopBody
(0,0): anon7_Then
Definedness.dfy(143,15): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(143,5): anon8_LoopHead
(0,0): anon8_LoopBody
Definedness.dfy(143,5): anon9_Else
Definedness.dfy(162,15): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(156,5): anon16_LoopHead
(0,0): anon16_LoopBody
Definedness.dfy(156,5): anon17_Else
(0,0): anon18_Then
(0,0): anon5
(0,0): anon19_Then
Definedness.dfy(162,5): anon20_LoopHead
(0,0): anon20_LoopBody
Definedness.dfy(162,5): anon21_Else
Definedness.dfy(175,28): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
Definedness.dfy(181,17): Error: possible violation of function precondition
Definedness.dfy(79,16): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(173,5): anon18_LoopHead
(0,0): anon18_LoopBody
Definedness.dfy(173,5): anon19_Else
(0,0): anon20_Then
Definedness.dfy(180,5): anon21_LoopHead
(0,0): anon21_LoopBody
(0,0): anon22_Then
(0,0): anon23_Then
(0,0): anon11
Definedness.dfy(196,19): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(194,5): anon6_LoopHead
(0,0): anon6_LoopBody
(0,0): anon7_Then
Definedness.dfy(196,23): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
Definedness.dfy(196,28): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(194,5): anon6_LoopHead
(0,0): anon6_LoopBody
(0,0): anon7_Then
Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(217,46): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon5_Else
Definedness.dfy(224,22): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
Definedness.dfy(237,10): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(240,24): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon7_Then
(0,0): anon2
(0,0): anon8_Else
Dafny program verifier finished with 21 verified, 37 errors
|
