Revision a7062da6
Added by LĂ©lio Brun over 3 years ago
src/compiler_stages.ml | ||
---|---|---|
93 | 93 |
Global.main_node := main_node; |
94 | 94 |
try ignore (Corelang.node_from_name main_node) |
95 | 95 |
with Not_found -> |
96 |
Format.eprintf "Code generation error: %a@." Error.pp_error_msg
|
|
96 |
Format.eprintf "Code generation error: %a@." Error.pp |
|
97 | 97 |
Error.Main_not_found; |
98 |
raise (Error.Error (Location.dummy_loc, Error.Main_not_found)))
|
|
98 |
raise (Error.Error (Location.dummy, Error.Main_not_found))) |
|
99 | 99 |
in |
100 | 100 |
|
101 | 101 |
(* Perform inlining before any analysis *) |
... | ... | |
249 | 249 |
|
250 | 250 |
(* printing code *) |
251 | 251 |
let stage3 prog machine_code dependencies basename extension = |
252 |
let open Options in |
|
252 | 253 |
let basename = Filename.basename basename in |
253 |
match !Options.output, extension with
|
|
254 |
| "C", ".lus" ->
|
|
254 |
match !output, extension with |
|
255 |
| OutC, ".lus" ->
|
|
255 | 256 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,"); |
256 | 257 |
C_backend.translate_to_c !generate_c_header |
257 | 258 |
(* alloc_header_file source_lib_file source_main_file makefile_file *) |
... | ... | |
260 | 261 |
ACSL annotations generation@,"); ACSL_backend.translate_to_acsl (* |
261 | 262 |
alloc_header_file source_lib_file source_main_file makefile_file *) |
262 | 263 |
basename prog machine_code dependencies end *) |
263 |
| "C", _ ->
|
|
264 |
| OutC, _ ->
|
|
264 | 265 |
C_backend.print_c_header basename; |
265 | 266 |
Log.report ~level:1 (fun fmt -> |
266 | 267 |
fprintf fmt ".. no C code generation for lusi@,") |
267 |
| "java", _ ->
|
|
268 |
| OutJava, _ ->
|
|
268 | 269 |
Format.eprintf "internal error: sorry, but not yet supported !"; |
269 | 270 |
assert false |
270 | 271 |
(*let source_file = basename ^ ".java" in Log.report ~level:1 (fun fmt -> |
... | ... | |
273 | 274 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?"); |
274 | 275 |
Java_backend.translate_to_java source_fmt basename normalized_prog |
275 | 276 |
machine_code;*) |
276 |
| "Ada", _ ->
|
|
277 |
| OutAda, _ ->
|
|
277 | 278 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@."); |
278 | 279 |
Ada_backend.translate_to_ada basename |
279 | 280 |
(Machine_code_common.arrow_machine :: machine_code) |
280 |
| "horn", _ ->
|
|
281 |
| OutHorn, _ ->
|
|
281 | 282 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
282 | 283 |
let source_file = destname ^ ".smt2" in |
283 | 284 |
(* Could be changed *) |
... | ... | |
294 | 295 |
let fmt = formatter_of_out_channel traces_out in |
295 | 296 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,"); |
296 | 297 |
Horn_backend_traces.traces_file fmt machine_code) |
297 |
| "lustre", _ ->
|
|
298 |
| OutLustre, _ ->
|
|
298 | 299 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
299 | 300 |
let source_file = destname ^ ".lustrec" ^ extension in |
300 | 301 |
(* Could be changed *) |
... | ... | |
306 | 307 |
Format.fprintf fmt "@.@?"; |
307 | 308 |
(* Lustre_backend.translate fmt basename normalized_prog machine_code *) |
308 | 309 |
() |
309 |
| "emf", _ ->
|
|
310 |
| OutEMF, _ ->
|
|
310 | 311 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
311 | 312 |
let source_file = destname ^ ".json" in |
312 | 313 |
(* Could be changed *) |
... | ... | |
314 | 315 |
let fmt = formatter_of_out_channel source_out in |
315 | 316 |
EMF_backend.translate fmt basename prog machine_code; |
316 | 317 |
() |
317 |
| _ -> |
|
318 |
assert false |
Also available in: Unified diff
another step towards refactoring