Project

General

Profile

Revision e41592cf src/main_lustre_compiler.ml

View differences:

src/main_lustre_compiler.ml
299 299
	let source_file = destname ^ ".smt2" in (* Could be changed *)
300 300
	let source_out = open_out source_file in
301 301
	let fmt = formatter_of_out_channel source_out in
302
        Log.report ~level:1 (fun fmt -> fprintf fmt "@.. hornification@,");
302 303
	Horn_backend.translate fmt basename prog machine_code;
303 304
	(* Tracability file if option is activated *)
304 305
	if !Options.traces then (
305
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
306
	let traces_out = open_out traces_file in
307
	let fmt = formatter_of_out_channel traces_out in
308
	Horn_backend.traces_file fmt basename prog machine_code;
306
	  let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
307
	  let traces_out = open_out traces_file in
308
	  let fmt = formatter_of_out_channel traces_out in
309
          Log.report ~level:1 (fun fmt -> fprintf fmt "@.. tracing info@,");
310
	  Horn_backend.traces_file fmt basename prog machine_code;
309 311
	)
310 312
      end
311 313
    | "lustre" ->
......
321 323
    | _ -> assert false
322 324
  in
323 325
  begin
324
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
326
    Log.report ~level:1 (fun fmt -> fprintf fmt "@.. done @ @]@.");
325 327
  (* We stop the process here *)
326 328
    exit 0
327 329
  end

Also available in: Unified diff