Revision a7062da6
Added by LĂ©lio Brun over 3 years ago
src/backends/C/c_backend_spec.ml | ||
---|---|---|
17 | 17 |
open Spec_types |
18 | 18 |
open Machine_code_common |
19 | 19 |
|
20 |
module Mpfr = Lustrec_mpfr |
|
21 |
|
|
20 | 22 |
(**************************************************************************) |
21 | 23 |
(* Printing spec for c *) |
22 | 24 |
|
... | ... | |
508 | 510 |
((mp, (name, mem), (name, self)), mp.mpformula) |
509 | 511 |
|
510 | 512 |
let print_machine_ghost_struct fmt m = |
511 |
pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
|
|
513 |
pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m
|
|
512 | 514 |
|
513 | 515 |
let pp_memory_pack_defs fmt m = |
514 | 516 |
if not (fst (get_stateless_status m)) then |
... | ... | |
900 | 902 |
"\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \ |
901 | 903 |
%s_main_eacsl.o %a@." |
902 | 904 |
basename |
903 |
(Utils.fprintf_list ~sep:" " (fun fmt dep -> |
|
904 |
Format.fprintf fmt "%s.o" dep.name)) |
|
905 |
(pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name)) |
|
905 | 906 |
(C_backend_makefile.compiled_dependencies dependencies) |
906 | 907 |
("${FRAMACEACSL}/e_acsl.c " |
907 | 908 |
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c " |
908 | 909 |
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c") |
909 | 910 |
basename |
910 |
(Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
|
|
911 |
(pp_print_list (fun fmt lib -> fprintf fmt "-l%s" lib))
|
|
911 | 912 |
(C_backend_makefile.lib_dependencies dependencies); |
912 | 913 |
fprintf fmt "@." |
913 | 914 |
end |
Also available in: Unified diff
another step towards refactoring