source: driver/extracted/rTLabs_traces.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 34.4 KB
Line 
1open Preamble
2
3open Deqsets_extra
4
5open CostSpec
6
7open Sets
8
9open Listb
10
11open StructuredTraces
12
13open BitVectorTrie
14
15open Graphs
16
17open Order
18
19open Registers
20
21open FrontEndOps
22
23open RTLabs_syntax
24
25open SmallstepExec
26
27open CostLabel
28
29open Events
30
31open IOMonad
32
33open IO
34
35open Extra_bool
36
37open Coqlib
38
39open Values
40
41open FrontEndVal
42
43open Hide
44
45open ByteValues
46
47open Division
48
49open Z
50
51open BitVectorZ
52
53open Pointers
54
55open GenMem
56
57open FrontEndMem
58
59open Proper
60
61open PositiveMap
62
63open Deqsets
64
65open Extralib
66
67open Lists
68
69open Identifiers
70
71open Exp
72
73open Arithmetic
74
75open Vector
76
77open Div_and_mod
78
79open Util
80
81open FoldStuff
82
83open BitVector
84
85open Extranat
86
87open Integers
88
89open AST
90
91open Globalenvs
92
93open ErrorMessages
94
95open Option
96
97open Setoids
98
99open Monad
100
101open Jmeq
102
103open Russell
104
105open Positive
106
107open PreIdentifiers
108
109open Errors
110
111open Bool
112
113open Relations
114
115open Nat
116
117open Hints_declaration
118
119open Core_notation
120
121open Pts
122
123open Logic
124
125open Types
126
127open List
128
129open RTLabs_semantics
130
131open RTLabs_abstract
132
133open CostMisc
134
135open Executions
136
137open Listb_extra
138
139type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t
140and ('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
144
145val 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
150
151val 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
156
157val 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
162
163val 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
168
169val 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
174
175val flat_trace_discr :
176  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
177  ('a1, 'a2) flat_trace -> __
178
179val flat_trace_jmdiscr :
180  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
181  ('a1, 'a2) flat_trace -> __
182
183val make_flat_trace :
184  __ -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace
185
186val make_whole_flat_trace : __ -> __ -> (IO.io_out, IO.io_in) flat_trace
187
188type will_return =
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
197
198val 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
210
211val 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
223
224val 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
236
237val 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
249
250val 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
262
263val 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
277
278val 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
292
293val 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
307
308val 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
322
323val 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
337
338val 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 -> __
341
342val 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
345
346val 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
350
351val 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
355
356val 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 ->
359  will_return -> __
360
361val 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
365
366val 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
370
371val nat_jmdiscr : Nat.nat -> Nat.nat -> __
372
373val 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
377
378val 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
381
382val list_jmdiscr : 'a1 List.list -> 'a1 List.list -> __
383
384type '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 : __ }
387
388val 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
393  -> 'a2
394
395val 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
400  -> 'a2
401
402val 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
407  -> 'a2
408
409val 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
414  -> 'a2
415
416val 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
421  -> 'a2
422
423val 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
428  -> 'a2
429
430val new_state :
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
435
436val remainder :
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)
440  flat_trace
441
442val new_trace :
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
446
447val terminates :
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 -> __
451
452val 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
458
459val 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
465
466val 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
472
473val 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
479
480val 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
486
487val 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 -> __
491
492type 't sub_trace_result = { ends : StructuredTraces.trace_ends_with_ret;
493                             trace_res : 't trace_result }
494
495val 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
500
501val 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
506
507val 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
512
513val 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
518
519val 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
524
525val 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
530
531val ends :
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
535
536val trace_res :
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
540
541val 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
546
547val 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
552
553val 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
558
559val 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
564
565val 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
570
571val 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 -> __
575
576val 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 -> __
580
581val replace_trace :
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
586  -> 'a2 trace_result
587
588val 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
593
594val make_any_label :
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
598
599val 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
603
604val 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
608
609val 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
613
614val actual_successor : RTLabs_semantics.state -> Graphs.label Types.option
615
616val steps_for_statement : RTLabs_syntax.statement -> Nat.nat
617
618type remainder_ok =
619| Mk_remainder_ok
620
621val 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 ->
624  'a1
625
626val 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 ->
629  'a1
630
631val 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 ->
634  'a1
635
636val 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 ->
639  'a1
640
641val 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 ->
644  'a1
645
646val 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 ->
649  'a1
650
651val 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)
654  -> 'a1
655
656val 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)
659  -> 'a1
660
661val 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)
664  -> 'a1
665
666val 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)
669  -> 'a1
670
671val 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)
674  -> 'a1
675
676val 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 -> __
679
680val 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 -> __
683
684val init_state_is :
685  RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state -> (Pointers.block,
686  __) Types.dPair
687
688val ras_state_initial :
689  RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
690  RTLabs_abstract.rTLabs_ext_state
691
692val deprop_execute :
693  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
694  -> Events.trace Types.sig0
695
696val deprop_as_execute :
697  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
698  RTLabs_abstract.rTLabs_ext_state -> Events.trace Types.sig0
699
700type ('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
704
705val 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
711
712val 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
718
719val 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
725
726val 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
732
733val 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
739
740val 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
747
748val 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
755
756val 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
763
764val 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
771
772val 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
779
780val 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 -> __
783
784val 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
788
789val 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)
792  flat_trace
793
794val 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)
798  partial_flat_trace
799
800val 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)
804  partial_flat_trace
805
806val 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
810
811val 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)
815  partial_flat_trace
816
817val 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)
821  partial_flat_trace
822
823val 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,
827  IO.io_in) flat_trace
828
829val 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
832
833val 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
836
837val state_fn : RTLabs_semantics.genv -> __ -> Pointers.block Types.option
838
839val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __
840
Note: See TracBrowser for help on using the repository browser.