1 |
a7062da6
|
Lélio Brun
|
open Utils
|
2 |
|
|
open Format
|
3 |
|
|
open Lustre_types
|
4 |
|
|
open Machine_code_types
|
5 |
|
|
open C_backend_common
|
6 |
|
|
|
7 |
|
|
module type MODIFIERS_SRC = sig
|
8 |
|
|
module GhostProto : MODIFIERS_GHOST_PROTO
|
9 |
|
|
|
10 |
|
|
val pp_predicates : formatter -> machine_t list -> unit
|
11 |
|
|
|
12 |
|
|
val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
|
13 |
|
|
|
14 |
|
|
val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
|
15 |
|
|
|
16 |
|
|
val pp_step_spec :
|
17 |
|
|
formatter -> machine_t list -> ident -> ident -> machine_t -> unit
|
18 |
|
|
|
19 |
|
|
val pp_step_instr_spec :
|
20 |
|
|
machine_t -> ident -> ident -> formatter -> instr_t -> unit
|
21 |
|
|
|
22 |
|
|
val pp_ghost_parameter : ident -> formatter -> ident option -> unit
|
23 |
5b98398a
|
Lélio Brun
|
|
24 |
d29fbec5
|
Lélio Brun
|
val pp_contract :
|
25 |
|
|
formatter -> machine_t list -> ident -> ident -> machine_t -> unit
|
26 |
a7062da6
|
Lélio Brun
|
end
|
27 |
|
|
|
28 |
|
|
module EmptyMod : MODIFIERS_SRC
|
29 |
|
|
|
30 |
|
|
module Main (Mod : MODIFIERS_SRC) : sig
|
31 |
d978c46e
|
Lélio Brun
|
val pp_lib_c :
|
32 |
cc852504
|
Lélio Brun
|
formatter -> string -> program_t -> machine_t list -> dep_t list -> unit
|
33 |
a7062da6
|
Lélio Brun
|
end
|