121 open MemoryInjections
243 open Hints_declaration
269 open Clight_classified_system
271 open Cminor_semantics
275 open Cminor_classified_system
277 open RTLabs_semantics
281 open RTLabs_classified_system
303 open Joint_LTL_LIN_semantics
311 type preclassified_system_pass =
312 Measurable.preclassified_system
313 (* singleton inductive, whose constructor was mk_preclassified_system_pass *)
315 val preclassified_system_pass_rect_Type4 :
316 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
317 preclassified_system_pass -> 'a1
319 val preclassified_system_pass_rect_Type5 :
320 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
321 preclassified_system_pass -> 'a1
323 val preclassified_system_pass_rect_Type3 :
324 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
325 preclassified_system_pass -> 'a1
327 val preclassified_system_pass_rect_Type2 :
328 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
329 preclassified_system_pass -> 'a1
331 val preclassified_system_pass_rect_Type1 :
332 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
333 preclassified_system_pass -> 'a1
335 val preclassified_system_pass_rect_Type0 :
336 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
337 preclassified_system_pass -> 'a1
340 Compiler.pass -> preclassified_system_pass ->
341 Measurable.preclassified_system
343 val preclassified_system_pass_inv_rect_Type4 :
344 Compiler.pass -> preclassified_system_pass ->
345 (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
347 val preclassified_system_pass_inv_rect_Type3 :
348 Compiler.pass -> preclassified_system_pass ->
349 (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
351 val preclassified_system_pass_inv_rect_Type2 :
352 Compiler.pass -> preclassified_system_pass ->
353 (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
355 val preclassified_system_pass_inv_rect_Type1 :
356 Compiler.pass -> preclassified_system_pass ->
357 (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
359 val preclassified_system_pass_inv_rect_Type0 :
360 Compiler.pass -> preclassified_system_pass ->
361 (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1
363 val pcs_pcs__o__pcs_exec :
364 Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
365 SmallstepExec.fullexec
367 val pcs_pcs__o__pcs_exec__o__es1 :
368 Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
369 SmallstepExec.trans_system
371 val preclassified_system_of_pass :
372 Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass
375 Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
376 Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
377 (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->