117 open Hints_declaration
129 open RTLabs_semantics
139 type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t
140 and ('o, 'i) __flat_trace =
141 | Ft_stop of RTLabs_semantics.state
142 | Ft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
143 * ('o, 'i) flat_trace
145 val flat_trace_inv_rect_Type4 :
146 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
147 (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
148 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
149 ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
151 val flat_trace_inv_rect_Type3 :
152 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
153 (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
154 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
155 ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
157 val flat_trace_inv_rect_Type2 :
158 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
159 (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
160 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
161 ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
163 val flat_trace_inv_rect_Type1 :
164 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
165 (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
166 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
167 ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
169 val flat_trace_inv_rect_Type0 :
170 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
171 (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
172 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
173 ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
175 val flat_trace_discr :
176 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
177 ('a1, 'a2) flat_trace -> __
179 val flat_trace_jmdiscr :
180 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
181 ('a1, 'a2) flat_trace -> __
183 val make_flat_trace :
184 __ -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace
186 val make_whole_flat_trace : __ -> __ -> (IO.io_out, IO.io_in) flat_trace
189 | Wr_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
190 * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
191 | Wr_call of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
192 * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
193 | Wr_ret of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
194 * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
195 | Wr_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
196 * (IO.io_out, IO.io_in) flat_trace
198 val will_return_rect_Type4 :
199 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
200 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
201 -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
202 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
203 IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
204 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
205 Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
206 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
207 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
208 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
209 flat_trace -> will_return -> 'a1
211 val will_return_rect_Type3 :
212 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
213 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
214 -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
215 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
216 IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
217 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
218 Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
219 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
220 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
221 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
222 flat_trace -> will_return -> 'a1
224 val will_return_rect_Type2 :
225 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
226 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
227 -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
228 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
229 IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
230 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
231 Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
232 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
233 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
234 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
235 flat_trace -> will_return -> 'a1
237 val will_return_rect_Type1 :
238 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
239 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
240 -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
241 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
242 IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
243 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
244 Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
245 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
246 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
247 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
248 flat_trace -> will_return -> 'a1
250 val will_return_rect_Type0 :
251 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
252 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
253 -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
254 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
255 IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
256 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
257 Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
258 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
259 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
260 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
261 flat_trace -> will_return -> 'a1
263 val will_return_inv_rect_Type4 :
264 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
265 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
266 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
267 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
268 -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
269 -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
270 flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
271 __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
272 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
273 -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
274 __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
275 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
276 __ -> __ -> __ -> __ -> 'a1) -> 'a1
278 val will_return_inv_rect_Type3 :
279 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
280 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
281 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
282 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
283 -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
284 -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
285 flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
286 __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
287 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
288 -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
289 __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
290 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
291 __ -> __ -> __ -> __ -> 'a1) -> 'a1
293 val will_return_inv_rect_Type2 :
294 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
295 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
296 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
297 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
298 -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
299 -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
300 flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
301 __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
302 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
303 -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
304 __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
305 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
306 __ -> __ -> __ -> __ -> 'a1) -> 'a1
308 val will_return_inv_rect_Type1 :
309 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
310 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
311 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
312 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
313 -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
314 -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
315 flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
316 __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
317 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
318 -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
319 __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
320 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
321 __ -> __ -> __ -> __ -> 'a1) -> 'a1
323 val will_return_inv_rect_Type0 :
324 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
325 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
326 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
327 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
328 -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
329 -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
330 flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
331 __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
332 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
333 -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
334 __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
335 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
336 __ -> __ -> __ -> __ -> 'a1) -> 'a1
338 val will_return_jmdiscr :
339 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
340 IO.io_in) flat_trace -> will_return -> will_return -> __
342 val will_return_length :
343 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
344 IO.io_in) flat_trace -> will_return -> Nat.nat
346 val will_return_end :
347 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
348 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state, (IO.io_out,
349 IO.io_in) flat_trace) Types.dPair
351 val will_return_call :
352 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
353 -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace ->
354 will_return -> will_return Types.sig0
356 val will_return_return :
357 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
358 -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace ->
361 val will_return_notfn :
362 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
363 -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> (__, __)
364 Types.sum -> will_return -> will_return Types.sig0
366 val will_return_prepend :
367 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
368 IO.io_in) flat_trace -> will_return -> Nat.nat -> RTLabs_semantics.state ->
369 (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return
371 val nat_jmdiscr : Nat.nat -> Nat.nat -> __
373 val will_return_remove_call :
374 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
375 IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return ->
376 RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return
378 val will_return_lower :
379 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
380 IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return
382 val list_jmdiscr : 'a1 List.list -> 'a1 List.list -> __
384 type 't trace_result = { new_state : RTLabs_abstract.rTLabs_ext_state;
385 remainder : (IO.io_out, IO.io_in) flat_trace;
386 new_trace : 't; terminates : __ }
388 val trace_result_rect_Type4 :
389 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
390 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
391 will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
392 IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
395 val trace_result_rect_Type5 :
396 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
397 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
398 will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
399 IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
402 val trace_result_rect_Type3 :
403 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
404 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
405 will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
406 IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
409 val trace_result_rect_Type2 :
410 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
411 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
412 will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
413 IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
416 val trace_result_rect_Type1 :
417 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
418 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
419 will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
420 IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
423 val trace_result_rect_Type0 :
424 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
425 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
426 will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
427 IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
431 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
432 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
433 will_return -> Nat.nat -> 'a1 trace_result ->
434 RTLabs_abstract.rTLabs_ext_state
437 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
438 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
439 will_return -> Nat.nat -> 'a1 trace_result -> (IO.io_out, IO.io_in)
443 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
444 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
445 will_return -> Nat.nat -> 'a1 trace_result -> 'a1
448 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
449 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
450 will_return -> Nat.nat -> 'a1 trace_result -> __
452 val trace_result_inv_rect_Type4 :
453 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
454 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
455 will_return -> Nat.nat -> 'a1 trace_result ->
456 (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
457 -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2
459 val trace_result_inv_rect_Type3 :
460 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
461 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
462 will_return -> Nat.nat -> 'a1 trace_result ->
463 (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
464 -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2
466 val trace_result_inv_rect_Type2 :
467 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
468 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
469 will_return -> Nat.nat -> 'a1 trace_result ->
470 (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
471 -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2
473 val trace_result_inv_rect_Type1 :
474 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
475 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
476 will_return -> Nat.nat -> 'a1 trace_result ->
477 (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
478 -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2
480 val trace_result_inv_rect_Type0 :
481 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
482 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
483 will_return -> Nat.nat -> 'a1 trace_result ->
484 (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
485 -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2
487 val trace_result_jmdiscr :
488 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
489 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
490 will_return -> Nat.nat -> 'a1 trace_result -> 'a1 trace_result -> __
492 type 't sub_trace_result = { ends : StructuredTraces.trace_ends_with_ret;
493 trace_res : 't trace_result }
495 val sub_trace_result_rect_Type4 :
496 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
497 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
498 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
499 sub_trace_result -> 'a2
501 val sub_trace_result_rect_Type5 :
502 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
503 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
504 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
505 sub_trace_result -> 'a2
507 val sub_trace_result_rect_Type3 :
508 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
509 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
510 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
511 sub_trace_result -> 'a2
513 val sub_trace_result_rect_Type2 :
514 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
515 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
516 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
517 sub_trace_result -> 'a2
519 val sub_trace_result_rect_Type1 :
520 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
521 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
522 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
523 sub_trace_result -> 'a2
525 val sub_trace_result_rect_Type0 :
526 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
527 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
528 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
529 sub_trace_result -> 'a2
532 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
533 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
534 sub_trace_result -> StructuredTraces.trace_ends_with_ret
537 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
538 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
539 sub_trace_result -> 'a1 trace_result
541 val sub_trace_result_inv_rect_Type4 :
542 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
543 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
544 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
545 trace_result -> __ -> 'a2) -> 'a2
547 val sub_trace_result_inv_rect_Type3 :
548 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
549 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
550 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
551 trace_result -> __ -> 'a2) -> 'a2
553 val sub_trace_result_inv_rect_Type2 :
554 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
555 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
556 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
557 trace_result -> __ -> 'a2) -> 'a2
559 val sub_trace_result_inv_rect_Type1 :
560 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
561 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
562 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
563 trace_result -> __ -> 'a2) -> 'a2
565 val sub_trace_result_inv_rect_Type0 :
566 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
567 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
568 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
569 trace_result -> __ -> 'a2) -> 'a2
571 val sub_trace_result_discr :
572 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
573 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
574 sub_trace_result -> 'a1 sub_trace_result -> __
576 val sub_trace_result_jmdiscr :
577 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
578 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
579 sub_trace_result -> 'a1 sub_trace_result -> __
582 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
583 RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
584 (IO.io_out, IO.io_in) flat_trace -> (IO.io_out, IO.io_in) flat_trace ->
585 will_return -> will_return -> Nat.nat -> Nat.nat -> 'a1 trace_result -> 'a2
588 val replace_sub_trace :
589 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
590 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
591 (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> Nat.nat
592 -> Nat.nat -> 'a1 sub_trace_result -> 'a2 -> 'a2 sub_trace_result
595 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
596 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
597 StructuredTraces.trace_any_label sub_trace_result
599 val make_label_label :
600 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
601 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
602 StructuredTraces.trace_label_label sub_trace_result
604 val make_label_return :
605 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
606 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
607 StructuredTraces.trace_label_return trace_result
609 val make_label_return' :
610 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
611 (IO.io_out, IO.io_in) flat_trace -> will_return ->
612 StructuredTraces.trace_label_return trace_result
614 val actual_successor : RTLabs_semantics.state -> Graphs.label Types.option
616 val steps_for_statement : RTLabs_syntax.statement -> Nat.nat
621 val remainder_ok_rect_Type4 :
622 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
623 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
626 val remainder_ok_rect_Type5 :
627 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
628 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
631 val remainder_ok_rect_Type3 :
632 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
633 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
636 val remainder_ok_rect_Type2 :
637 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
638 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
641 val remainder_ok_rect_Type1 :
642 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
643 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
646 val remainder_ok_rect_Type0 :
647 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
648 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
651 val remainder_ok_inv_rect_Type4 :
652 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
653 IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
656 val remainder_ok_inv_rect_Type3 :
657 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
658 IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
661 val remainder_ok_inv_rect_Type2 :
662 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
663 IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
666 val remainder_ok_inv_rect_Type1 :
667 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
668 IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
671 val remainder_ok_inv_rect_Type0 :
672 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
673 IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
676 val remainder_ok_discr :
677 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
678 IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __
680 val remainder_ok_jmdiscr :
681 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
682 IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __
685 RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state -> (Pointers.block,
688 val ras_state_initial :
689 RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
690 RTLabs_abstract.rTLabs_ext_state
693 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
694 -> Events.trace Types.sig0
696 val deprop_as_execute :
697 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
698 RTLabs_abstract.rTLabs_ext_state -> Events.trace Types.sig0
700 type ('o, 'i) partial_flat_trace =
701 | Pft_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
702 | Pft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
703 * RTLabs_semantics.state * ('o, 'i) partial_flat_trace
705 val partial_flat_trace_rect_Type4 :
706 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
707 RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
708 Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
709 ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
710 RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3
712 val partial_flat_trace_rect_Type3 :
713 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
714 RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
715 Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
716 ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
717 RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3
719 val partial_flat_trace_rect_Type2 :
720 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
721 RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
722 Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
723 ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
724 RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3
726 val partial_flat_trace_rect_Type1 :
727 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
728 RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
729 Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
730 ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
731 RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3
733 val partial_flat_trace_rect_Type0 :
734 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
735 RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
736 Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
737 ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
738 RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3
740 val partial_flat_trace_inv_rect_Type4 :
741 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
742 -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
743 -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
744 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
745 RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
746 -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
748 val partial_flat_trace_inv_rect_Type3 :
749 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
750 -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
751 -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
752 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
753 RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
754 -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
756 val partial_flat_trace_inv_rect_Type2 :
757 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
758 -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
759 -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
760 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
761 RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
762 -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
764 val partial_flat_trace_inv_rect_Type1 :
765 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
766 -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
767 -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
768 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
769 RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
770 -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
772 val partial_flat_trace_inv_rect_Type0 :
773 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
774 -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
775 -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
776 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
777 RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
778 -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
780 val partial_flat_trace_jmdiscr :
781 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
782 -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> __
784 val append_partial_flat_trace :
785 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
786 -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
787 partial_flat_trace -> ('a1, 'a2) partial_flat_trace
789 val partial_to_flat_trace :
790 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
791 -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) flat_trace -> ('a1, 'a2)
794 val flat_trace_of_any_label :
795 RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
796 RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
797 StructuredTraces.trace_any_label -> (IO.io_out, IO.io_in)
800 val flat_trace_of_label_label :
801 RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
802 RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
803 StructuredTraces.trace_label_label -> (IO.io_out, IO.io_in)
806 val flat_trace_of_label_return :
807 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
808 RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_return ->
809 (IO.io_out, IO.io_in) partial_flat_trace
811 val flat_trace_of_any_call :
812 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
813 RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
814 Events.trace -> StructuredTraces.trace_any_call -> (IO.io_out, IO.io_in)
817 val flat_trace_of_label_call :
818 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
819 RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
820 Events.trace -> StructuredTraces.trace_label_call -> (IO.io_out, IO.io_in)
823 val add_partial_flat_trace :
824 RTLabs_semantics.genv -> RTLabs_semantics.state ->
825 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in)
826 partial_flat_trace -> StructuredTraces.trace_label_diverges -> (IO.io_out,
829 val flat_trace_of_label_diverges :
830 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
831 StructuredTraces.trace_label_diverges -> (IO.io_out, IO.io_in) flat_trace
833 val flat_trace_of_whole_program :
834 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
835 StructuredTraces.trace_whole_program -> (IO.io_out, IO.io_in) flat_trace
837 val state_fn : RTLabs_semantics.genv -> __ -> Pointers.block Types.option
839 val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __