Project

General

Profile

Revision dc893173

View differences:

src/backends/C/c_backend.ml
25 25
  )
26 26
*)
27 27

  
28
let gen_files funs basename prog machines dependencies header_file source_lib_file source_main_file makefile_file machines =
29

  
30
  let header_out = open_out header_file in
31
  let header_fmt = formatter_of_out_channel header_out in
32
  let source_lib_out = open_out source_lib_file in
33
  let source_lib_fmt = formatter_of_out_channel source_lib_out in
34

  
28
let gen_files funs basename prog machines dependencies =
29
  let destname = !Options.dest_dir ^ "/" ^ basename in
30
  let source_main_file = destname ^ "_main.c" in (* Could be changed *)
31
  let makefile_file = destname ^ ".makefile" in (* Could be changed *)
32
  
35 33
  let print_header, print_lib_c, print_main_c, print_makefile = funs in
34

  
36 35
  (* Generating H file *)
36
  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
37
  let header_out = open_out alloc_header_file in
38
  let header_fmt = formatter_of_out_channel header_out in
37 39
  print_header header_fmt basename prog machines dependencies;
38
 
40
  close_out header_out;
41
  
39 42
  (* Generating Lib C file *)
43
  let source_lib_file = destname ^ ".c" in (* Could be changed *)
44
  let source_lib_out = open_out source_lib_file in
45
  let source_lib_fmt = formatter_of_out_channel source_lib_out in
40 46
  print_lib_c source_lib_fmt basename prog machines dependencies;
41

  
42
  close_out header_out;
43 47
  close_out source_lib_out;
44 48

  
45 49
  match !Options.main_node with
......
69 73
    end
70 74
  )
71 75

  
72
let translate_to_c header source_lib source_main makefile basename prog machines dependencies =
76
let translate_to_c basename prog machines dependencies =
73 77
  match !Options.spec with
74 78
  | "no" -> begin
75 79
    let module HeaderMod = C_backend_header.EmptyMod in
......
88 92
      SourceMain.print_main_c, 
89 93
      Makefile.print_makefile 
90 94
    in
91
    gen_files 
92
      funs basename prog machines dependencies 
93
      header source_lib source_main makefile machines
95
    gen_files funs basename prog machines dependencies 
94 96

  
95 97
  end
96 98
  | "acsl" -> begin
......
111 113
      SourceMain.print_main_c,
112 114
      Makefile.print_makefile 
113 115
    in
114
    gen_files
115
      funs basename prog machines dependencies
116
      header source_lib source_main makefile machines
116
    gen_files funs basename prog machines dependencies 
117 117

  
118 118
  end
119 119
  | "c" -> begin
src/main_lustre_compiler.ml
324 324
(* printing code *)
325 325
let stage3 prog machine_code dependencies basename =
326 326
  let basename    =  Filename.basename basename in
327
  let destname = !Options.dest_dir ^ "/" ^ basename in
328 327
  match !Options.output with
329
      "C" -> 
330
	begin
331
	  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
332
	  let source_lib_file = destname ^ ".c" in (* Could be changed *)
333
	  let source_main_file = destname ^ "_main.c" in (* Could be changed *)
334
	  let makefile_file = destname ^ ".makefile" in (* Could be changed *)
335
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
336
	  C_backend.translate_to_c
337
	    alloc_header_file source_lib_file source_main_file makefile_file
338
	    basename prog machine_code dependencies
339
	end
340
    | "java" ->
341
      begin
342
	(Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
343
    (*let source_file = basename ^ ".java" in
344
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
345
      let source_out = open_out source_file in
346
      let source_fmt = formatter_of_out_channel source_out in
347
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
348
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
349
      end
350
    | "horn" ->
351
      begin
352
	let source_file = destname ^ ".smt2" in (* Could be changed *)
353
	let source_out = open_out source_file in
354
	let fmt = formatter_of_out_channel source_out in
355
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
356
        Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
357
	(* Tracability file if option is activated *)
358
	if !Options.traces then (
359
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
360
	let traces_out = open_out traces_file in
361
	let fmt = formatter_of_out_channel traces_out in
362
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
363
	Horn_backend_traces.traces_file fmt basename prog machine_code;
364
	)
365
      end
366
    | "lustre" ->
328
    "C" -> 
367 329
      begin
368
	let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
369
	let source_out = open_out source_file in
370
	let fmt = formatter_of_out_channel source_out in
371
	Printers.pp_prog fmt prog;
372
(*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
373
	()
330
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
331
	C_backend.translate_to_c
332
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
333
	  basename prog machine_code dependencies
374 334
      end
375

  
376
    | _ -> assert false
335
  | "java" ->
336
     begin
337
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
338
     (*let source_file = basename ^ ".java" in
339
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
340
       let source_out = open_out source_file in
341
       let source_fmt = formatter_of_out_channel source_out in
342
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
343
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
344
     end
345
  | "horn" ->
346
     begin
347
       let destname = !Options.dest_dir ^ "/" ^ basename in
348
       let source_file = destname ^ ".smt2" in (* Could be changed *)
349
       let source_out = open_out source_file in
350
       let fmt = formatter_of_out_channel source_out in
351
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
352
       Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
353
       (* Tracability file if option is activated *)
354
       if !Options.traces then (
355
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
356
	 let traces_out = open_out traces_file in
357
	 let fmt = formatter_of_out_channel traces_out in
358
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
359
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
360
       )
361
     end
362
  | "lustre" ->
363
     begin
364
       let destname = !Options.dest_dir ^ "/" ^ basename in
365
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
366
       let source_out = open_out source_file in
367
       let fmt = formatter_of_out_channel source_out in
368
       Printers.pp_prog fmt prog;
369
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
370
       ()
371
     end
372

  
373
  | _ -> assert false
377 374

  
378 375
(* compile a .lus source file *)
379 376
let rec compile_source dirname basename extension =

Also available in: Unified diff