source: extracted/rTLabs_traces.mli @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 34.6 KB
Line 
1open Preamble
2
3open Deqsets_extra
4
5open CostSpec
6
7open Sets
8
9open Listb
10
11open StructuredTraces
12
13open Graphs
14
15open Order
16
17open Registers
18
19open FrontEndOps
20
21open RTLabs_syntax
22
23open SmallstepExec
24
25open BitVectorTrie
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.state0
142| Ft_step of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
143   * ('o, 'i) flat_trace
144
145val flat_trace_inv_rect_Type4 :
146  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
147  -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
148  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
149  -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
150
151val flat_trace_inv_rect_Type3 :
152  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
153  -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
154  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
155  -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
156
157val flat_trace_inv_rect_Type2 :
158  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
159  -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
160  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
161  -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
162
163val flat_trace_inv_rect_Type1 :
164  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
165  -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
166  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
167  -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
168
169val flat_trace_inv_rect_Type0 :
170  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
171  -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
172  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
173  -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
174
175val flat_trace_discr :
176  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
177  -> ('a1, 'a2) flat_trace -> __
178
179val flat_trace_jmdiscr :
180  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
181  -> ('a1, 'a2) flat_trace -> __
182
183val make_flat_trace :
184  __ -> RTLabs_semantics.state0 -> (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.state0 * Events.trace * RTLabs_semantics.state0
190   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
191| Wr_call of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
192   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
193| Wr_ret of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
194   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
195| Wr_base of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
196   * (IO.io_out, IO.io_in) flat_trace
197
198val will_return_rect_Type4 :
199  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
200  RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
201  flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state0
202  -> Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
203  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
204  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
205  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
206  'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
207  RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
208  'a1) -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
209  flat_trace -> will_return -> 'a1
210
211val will_return_rect_Type3 :
212  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
213  RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
214  flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state0
215  -> Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
216  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
217  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
218  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
219  'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
220  RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
221  'a1) -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
222  flat_trace -> will_return -> 'a1
223
224val will_return_rect_Type2 :
225  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
226  RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
227  flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state0
228  -> Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
229  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
230  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
231  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
232  'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
233  RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
234  'a1) -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
235  flat_trace -> will_return -> 'a1
236
237val will_return_rect_Type1 :
238  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
239  RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
240  flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state0
241  -> Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
242  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
243  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
244  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
245  'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
246  RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
247  'a1) -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
248  flat_trace -> will_return -> 'a1
249
250val will_return_rect_Type0 :
251  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
252  RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
253  flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state0
254  -> Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
255  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
256  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
257  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
258  'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
259  RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
260  'a1) -> Nat.nat -> RTLabs_semantics.state0 -> (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.state0 -> (IO.io_out,
265  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0 ->
266  Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
267  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
268  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace
269  -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
270  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
271  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
272  RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
273  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
274  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
275  RTLabs_semantics.state0 -> __ -> (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.state0 -> (IO.io_out,
280  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0 ->
281  Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
282  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
283  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace
284  -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
285  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
286  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
287  RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
288  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
289  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
290  RTLabs_semantics.state0 -> __ -> (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.state0 -> (IO.io_out,
295  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0 ->
296  Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
297  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
298  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace
299  -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
300  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
301  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
302  RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
303  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
304  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
305  RTLabs_semantics.state0 -> __ -> (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.state0 -> (IO.io_out,
310  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0 ->
311  Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
312  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
313  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace
314  -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
315  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
316  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
317  RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
318  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
319  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
320  RTLabs_semantics.state0 -> __ -> (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.state0 -> (IO.io_out,
325  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0 ->
326  Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
327  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
328  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace
329  -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
330  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
331  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
332  RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
333  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
334  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
335  RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
336  __ -> __ -> __ -> __ -> 'a1) -> 'a1
337
338val will_return_jmdiscr :
339  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (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.state0 -> (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.state0 -> (IO.io_out,
348  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0,
349  (IO.io_out, IO.io_in) flat_trace) Types.dPair
350
351val will_return_call :
352  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> Events.trace
353  -> RTLabs_semantics.state0 -> (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.state0 -> Events.trace
358  -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
359  will_return -> __
360
361val will_return_notfn :
362  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> Events.trace
363  -> RTLabs_semantics.state0 -> (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.state0 -> (IO.io_out,
368  IO.io_in) flat_trace -> will_return -> Nat.nat -> RTLabs_semantics.state0
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.state0 -> (IO.io_out,
375  IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return ->
376  RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace -> will_return
377
378val will_return_lower :
379  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (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.state0 -> 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.state0 -> (Pointers.block,
686  __) Types.dPair
687
688val ras_state_initial :
689  RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state0 ->
690  RTLabs_abstract.rTLabs_ext_state
691
692val deprop_execute :
693  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
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.state0 * Events.trace
702   * RTLabs_semantics.state0
703| Pft_step of RTLabs_semantics.state0 * Events.trace
704   * RTLabs_semantics.state0 * RTLabs_semantics.state0
705   * ('o, 'i) partial_flat_trace
706
707val partial_flat_trace_rect_Type4 :
708  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
709  RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
710  Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ ->
711  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state0 ->
712  RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> 'a3
713
714val partial_flat_trace_rect_Type3 :
715  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
716  RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
717  Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ ->
718  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state0 ->
719  RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> 'a3
720
721val partial_flat_trace_rect_Type2 :
722  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
723  RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
724  Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ ->
725  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state0 ->
726  RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> 'a3
727
728val partial_flat_trace_rect_Type1 :
729  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
730  RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
731  Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ ->
732  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state0 ->
733  RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> 'a3
734
735val partial_flat_trace_rect_Type0 :
736  RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
737  RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
738  Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ ->
739  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state0 ->
740  RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> 'a3
741
742val partial_flat_trace_inv_rect_Type4 :
743  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
744  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state0 ->
745  Events.trace -> RTLabs_semantics.state0 -> __ -> __ -> __ -> __ -> 'a3) ->
746  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
747  RTLabs_semantics.state0 -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
748  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
749
750val partial_flat_trace_inv_rect_Type3 :
751  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
752  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state0 ->
753  Events.trace -> RTLabs_semantics.state0 -> __ -> __ -> __ -> __ -> 'a3) ->
754  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
755  RTLabs_semantics.state0 -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
756  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
757
758val partial_flat_trace_inv_rect_Type2 :
759  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
760  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state0 ->
761  Events.trace -> RTLabs_semantics.state0 -> __ -> __ -> __ -> __ -> 'a3) ->
762  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
763  RTLabs_semantics.state0 -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
764  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
765
766val partial_flat_trace_inv_rect_Type1 :
767  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
768  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state0 ->
769  Events.trace -> RTLabs_semantics.state0 -> __ -> __ -> __ -> __ -> 'a3) ->
770  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
771  RTLabs_semantics.state0 -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
772  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
773
774val partial_flat_trace_inv_rect_Type0 :
775  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
776  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state0 ->
777  Events.trace -> RTLabs_semantics.state0 -> __ -> __ -> __ -> __ -> 'a3) ->
778  (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
779  RTLabs_semantics.state0 -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
780  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
781
782val partial_flat_trace_jmdiscr :
783  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
784  -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> __
785
786val append_partial_flat_trace :
787  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
788  -> RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
789  partial_flat_trace -> ('a1, 'a2) partial_flat_trace
790
791val partial_to_flat_trace :
792  RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
793  -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) flat_trace -> ('a1, 'a2)
794  flat_trace
795
796val flat_trace_of_any_label :
797  RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
798  RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
799  StructuredTraces.trace_any_label -> (IO.io_out, IO.io_in)
800  partial_flat_trace
801
802val flat_trace_of_label_label :
803  RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
804  RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
805  StructuredTraces.trace_label_label -> (IO.io_out, IO.io_in)
806  partial_flat_trace
807
808val flat_trace_of_label_return :
809  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
810  RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_return ->
811  (IO.io_out, IO.io_in) partial_flat_trace
812
813val flat_trace_of_any_call :
814  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
815  RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
816  Events.trace -> StructuredTraces.trace_any_call -> (IO.io_out, IO.io_in)
817  partial_flat_trace
818
819val flat_trace_of_label_call :
820  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
821  RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
822  Events.trace -> StructuredTraces.trace_label_call -> (IO.io_out, IO.io_in)
823  partial_flat_trace
824
825val add_partial_flat_trace :
826  RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
827  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in)
828  partial_flat_trace -> StructuredTraces.trace_label_diverges -> (IO.io_out,
829  IO.io_in) flat_trace
830
831val flat_trace_of_label_diverges :
832  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
833  StructuredTraces.trace_label_diverges -> (IO.io_out, IO.io_in) flat_trace
834
835val flat_trace_of_whole_program :
836  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
837  StructuredTraces.trace_whole_program -> (IO.io_out, IO.io_in) flat_trace
838
839val state_fn : RTLabs_semantics.genv -> __ -> Pointers.block Types.option
840
841val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __
842
Note: See TracBrowser for help on using the repository browser.