Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
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
Merged horn_traces branch