Project

General

Profile

« Previous | Next » 

Revision efcc8d7f

Added by LĂ©lio Brun about 2 years ago

move arrow spec in its own header

View differences:

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