Project

General

Profile

Revision ad6b7375 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
	Horn_backend.translate fmt basename prog machine_code;
302
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
303
        Horn_backend.translate fmt basename prog machine_code;
303 304
	(* Tracability file if option is activated *)
304 305
	if !Options.traces then (
305 306
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
306 307
	let traces_out = open_out traces_file in
307 308
	let fmt = formatter_of_out_channel traces_out in
309
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
308 310
	Horn_backend.traces_file fmt basename prog machine_code;
309 311
	)
310 312
      end
......
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