Project

General

Profile

Revision f6923c9e

View differences:

src/c_backend.ml
819 819
  let main_include, main_print, main_makefile =
820 820
    match !Options.main_node with
821 821
      | "" -> (fun _ -> ()), (fun _ -> ()), (fun _ -> ())
822
      | main_node -> ( 
823
	let main_node_opt = 
824
	  List.fold_left 
825
	  (fun res m -> 
826
	    match res with 
827
	      | Some _ -> res 
828
	      | None -> if m.mname.node_id = main_node then Some m else None)
829
	  None machines
830
      in 
831
      match main_node_opt with
822
      | main_node -> (
823
	match Machine_code.get_machine_opt main_node machines with
832 824
	| None -> eprintf "Unable to find a main node named %s@.@?" main_node; (fun _ -> ()), (fun _ -> ()), (fun _ -> ())
833 825
	| Some m -> print_main_header, print_main_fun machines m, print_makefile basename !Options.main_node
834
    )
826
      )
835 827
  in
836 828
  main_include source_fmt;
837 829
  fprintf source_fmt "#include <stdlib.h>@.#include <assert.h>@.#include \"%s\"@.@." (basename^".h");
src/machine_code.ml
436 436
  let nodes = get_nodes decls in 
437 437
   (* What to do with Imported/Sensor/Actuators ? *)
438 438
   arrow_machine ::  List.map translate_decl nodes
439
 
439

  
440
let get_machine_opt name machines =  
441
  List.fold_left 
442
    (fun res m -> 
443
      match res with 
444
      | Some _ -> res 
445
      | None -> if m.mname.node_id = name then Some m else None)
446
    None machines
447
    
440 448

  
441 449
(* Local Variables: *)
442 450
(* compile-command:"make -C .." *)
src/main_lustre_compiler.ml
216 216

  
217 217
  (* Printing code *)
218 218
  let basename    = Filename.basename basename in
219
  if !Options.java then
220
    failwith "Sorry, but not yet supported !"
219
  let _ = match !Options.output with
220
      "C" -> 
221
	begin
222
	  let header_file = basename ^ ".h" in (* Could be changed *)
223
	  let source_file = basename ^ ".c" in (* Could be changed *)
224
	  let makefile_file = basename ^ ".makefile" in (* Could be changed *)
225
	  let spec_file_opt = if !Options.c_spec then 
226
	      (
227
		let spec_file = basename ^ "_spec.c" in
228
		report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s, %s and %s@,@?" header_file source_file spec_file);
229
		Some spec_file 
230
	      ) else (
231
		report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s and %s@,@?" header_file source_file);
232
		None 
233
	       )
234
	  in 
235
	  let header_out = open_out header_file in
236
	  let header_fmt = formatter_of_out_channel header_out in
237
	  let source_out = open_out source_file in
238
	  let source_fmt = formatter_of_out_channel source_out in
239
	  let makefile_out = open_out makefile_file in
240
	  let makefile_fmt = formatter_of_out_channel makefile_out in
241
	  let spec_fmt_opt = match spec_file_opt with
242
	      None -> None
243
	    | Some f -> Some (formatter_of_out_channel (open_out f))
244
	  in
245
	  report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,@?");
246
	  C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code;
247
	end
248
    | "java" -> begin
249
      failwith "Sorry, but not yet supported !"
221 250
    (*let source_file = basename ^ ".java" in
222 251
      report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
223 252
      let source_out = open_out source_file in
224 253
      let source_fmt = formatter_of_out_channel source_out in
225 254
      report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
226 255
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
227
  else begin
228
    let header_file = basename ^ ".h" in (* Could be changed *)
229
    let source_file = basename ^ ".c" in (* Could be changed *)
230
    let makefile_file = basename ^ ".makefile" in (* Could be changed *)
231
    let spec_file_opt = if !Options.c_spec then 
232
	(
233
	  let spec_file = basename ^ "_spec.c" in
234
	  report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s, %s and %s@,@?" header_file source_file spec_file);
235
	  Some spec_file 
236
	) else (
237
	  report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s and %s@,@?" header_file source_file);
238
	  None 
239
	 )
240
    in 
241
    let header_out = open_out header_file in
242
    let header_fmt = formatter_of_out_channel header_out in
243
    let source_out = open_out source_file in
244
    let source_fmt = formatter_of_out_channel source_out in
245
    let makefile_out = open_out makefile_file in
246
    let makefile_fmt = formatter_of_out_channel makefile_out in
247
    let spec_fmt_opt = match spec_file_opt with
248
	None -> None
249
      | Some f -> Some (formatter_of_out_channel (open_out f))
250
    in
251
    report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,@?");
252
    C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code;
253
  end;
256
    end
257
    | "horn" -> begin
258
      let fmt = Format.std_formatter in
259
      Horn_backend.translate fmt basename normalized_prog machine_code
260
    end
261
  in
254 262
  report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
255 263
  (* We stop the process here *)
256 264
  exit 0
src/options.ml
30 30
let ansi = ref false
31 31
let check = ref false
32 32
let c_spec = ref false
33
let java = ref false
33
let output = ref "C"
34 34
let dest_dir = ref ""
35 35
let verbose_level = ref 1
36 36

  
......
44 44
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds (default: no check)";
45 45
    "-c-spec", Arg.Set c_spec, 
46 46
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
47
    "-java", Arg.Set java, "generates Java output instead of C";
47
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
48
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
48 49
    "-print_types", Arg.Set print_types, "prints node types";
49 50
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";
50 51
    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";

Also available in: Unified diff