Revision 71999483
Added by Pierre-Loïc Garoche about 4 years ago
| src/backends/C/c_backend.ml | ||
|---|---|---|
| 29 | 29 |
let gen_files funs basename prog machines dependencies = |
| 30 | 30 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
| 31 | 31 |
|
| 32 |
let print_header, print_lib_c, print_main_c, print_makefile(* , print_cmake *) = funs in |
|
| 32 |
let print_header, print_lib_c, print_main_c, print_makefile, preprocess (* , print_cmake *) = funs in
|
|
| 33 | 33 |
|
| 34 |
let machines, spec = preprocess machines in |
|
| 35 |
|
|
| 34 | 36 |
(* Generating H file *) |
| 35 | 37 |
let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *) |
| 36 | 38 |
let header_out = open_out alloc_header_file in |
| 37 | 39 |
let header_fmt = formatter_of_out_channel header_out in |
| 38 |
print_header header_fmt basename prog machines dependencies; |
|
| 40 |
print_header header_fmt basename prog machines dependencies spec;
|
|
| 39 | 41 |
close_out header_out; |
| 40 | 42 |
|
| 41 | 43 |
(* Generating Lib C file *) |
| ... | ... | |
| 146 | 148 |
Header.print_alloc_header, |
| 147 | 149 |
Source.print_lib_c, |
| 148 | 150 |
SourceMain.print_main_c, |
| 149 |
Makefile.print_makefile(* , *) |
|
| 151 |
Makefile.print_makefile, |
|
| 152 |
(fun m -> m, []) |
|
| 150 | 153 |
(* CMakefile.print_makefile *) |
| 151 | 154 |
in |
| 152 | 155 |
gen_files funs basename prog machines dependencies |
| ... | ... | |
| 169 | 172 |
Header.print_alloc_header, |
| 170 | 173 |
Source.print_lib_c, |
| 171 | 174 |
SourceMain.print_main_c, |
| 172 |
Makefile.print_makefile(* , *) |
|
| 175 |
Makefile.print_makefile, |
|
| 176 |
C_backend_spec.preprocess_acsl |
|
| 173 | 177 |
(* CMakefile.print_makefile *) |
| 174 | 178 |
in |
| 175 | 179 |
gen_files funs basename prog machines dependencies |
Also available in: Unified diff
Cleaning C backend - removing unused functiions
Preparing for coming ACSL