Project

General

Profile

« Previous | Next » 

Revision a7062da6

Added by LĂ©lio Brun over 3 years ago

another step towards refactoring

View differences:

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