Revision efcc8d7f
Added by Lélio Brun over 3 years ago
| src/backends/C/c_backend.ml | ||
|---|---|---|
| 42 | 42 |
f m |
| 43 | 43 |
|
| 44 | 44 |
let gen_files |
| 45 |
(print_header, print_lib_c, print_main_c, print_makefile, preprocess (* , print_cmake *)) |
|
| 45 |
(print_alloc_header, print_lib_c, print_main_c, print_makefile, preprocess (* , print_cmake *))
|
|
| 46 | 46 |
basename prog machines dependencies = |
| 47 | 47 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
| 48 | 48 |
|
| 49 | 49 |
let machines, spec = preprocess machines in |
| 50 |
|
|
| 51 |
(* Generating H file *) |
|
| 50 |
|
|
| 51 |
(* Generating H alloc file *)
|
|
| 52 | 52 |
let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *) |
| 53 | 53 |
with_out_file alloc_header_file (fun header_fmt -> |
| 54 |
print_header header_fmt basename prog machines dependencies spec); |
|
| 54 |
print_alloc_header header_fmt basename prog machines dependencies spec);
|
|
| 55 | 55 |
|
| 56 | 56 |
(* Generating Lib C file *) |
| 57 | 57 |
let source_lib_file = c_or_cpp destname in |
| ... | ... | |
| 104 | 104 |
|
| 105 | 105 |
(* close_out makefile_out *) |
| 106 | 106 |
|
| 107 |
let print_c_header basename = |
|
| 108 |
let header_m = match !Options.spec with |
|
| 109 |
| "no" -> |
|
| 110 |
C_backend_header.(module EmptyMod : MODIFIERS_HDR) |
|
| 111 |
|
|
| 112 |
| "acsl" -> |
|
| 113 |
C_backend_header.(module C_backend_spec.HdrMod : MODIFIERS_HDR) |
|
| 114 |
|
|
| 115 |
| "c" -> assert false (* not implemented yet *) |
|
| 107 | 116 |
|
| 108 |
let translate_to_c basename prog machines dependencies = |
|
| 117 |
| _ -> assert false |
|
| 118 |
in |
|
| 119 |
let module Header = C_backend_header.Main (val header_m) in |
|
| 120 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
|
| 121 |
(* Generating H file *) |
|
| 122 |
let lusic = Lusic.read_lusic destname ".lusic" in |
|
| 123 |
let header_file = destname ^ ".h" in |
|
| 124 |
with_out_file header_file (fun header_fmt -> |
|
| 125 |
assert (not lusic.obsolete); |
|
| 126 |
Header.print_header_from_header header_fmt basename lusic.contents) |
|
| 127 |
|
|
| 128 |
let translate_to_c generate_c_header basename prog machines dependencies = |
|
| 109 | 129 |
let header_m, source_m, source_main_m, makefile_m, preprocess = |
| 110 | 130 |
match !Options.spec with |
| 111 | 131 |
| "no" -> |
| ... | ... | |
| 116 | 136 |
fun m -> m, [] |
| 117 | 137 |
|
| 118 | 138 |
| "acsl" -> |
| 119 |
C_backend_header.(module EmptyMod : MODIFIERS_HDR), |
|
| 120 |
(module C_backend_spec.SrcMod : C_backend_src.MODIFIERS_SRC), |
|
| 139 |
let open C_backend_spec in |
|
| 140 |
C_backend_header.(module HdrMod : MODIFIERS_HDR), |
|
| 141 |
C_backend_src.(module SrcMod : MODIFIERS_SRC), |
|
| 121 | 142 |
C_backend_main.(module EmptyMod : MODIFIERS_MAINSRC), |
| 122 |
(module C_backend_spec.MakefileMod : C_backend_makefile.MODIFIERS_MKF),
|
|
| 123 |
C_backend_spec.preprocess_acsl
|
|
| 143 |
C_backend_makefile.(module MakefileMod : MODIFIERS_MKF),
|
|
| 144 |
preprocess_acsl |
|
| 124 | 145 |
|
| 125 | 146 |
| "c" -> assert false (* not implemented yet *) |
| 126 | 147 |
|
| ... | ... | |
| 139 | 160 |
preprocess |
| 140 | 161 |
(* CMakefile.print_makefile *) |
| 141 | 162 |
in |
| 163 |
if generate_c_header then print_c_header basename; |
|
| 142 | 164 |
gen_files funs basename prog machines dependencies |
| 143 | 165 |
|
| 144 | 166 |
|
Also available in: Unified diff
move arrow spec in its own header