Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

src/main_lustre_compiler.ml
356 356
	let source_file = destname ^ ".smt2" in (* Could be changed *)
357 357
	let source_out = open_out source_file in
358 358
	let fmt = formatter_of_out_channel source_out in
359
	Horn_backend.translate fmt basename prog machine_code
359
	Horn_backend.translate fmt basename prog machine_code;
360
	(* Tracability file if option is activated *)
361
	if !Options.horntraces then (
362
	let traces_file = destname ^ ".traces" in (* Could be changed *)
363
	let traces_out = open_out traces_file in
364
	let fmt = formatter_of_out_channel traces_out in
365
	Horn_backend.traces_file fmt basename prog machine_code	  
366
	)
360 367
      end
361 368
    | "lustre" -> 
362 369
      begin

Also available in: Unified diff