Revision 84902260
Added by jbraine almost 6 years ago
| src/main_lustre_compiler.ml | ||
|---|---|---|
| 316 | 316 |
end |
| 317 | 317 |
| "horn" -> |
| 318 | 318 |
begin |
| 319 |
let source_file = destname ^ ".smt2" in (* Could be changed *) |
|
| 319 |
let source_file = if !Options.dest_file ="" then destname ^ ".smt2" else !Options.dest_file in (* Could be changed *) |
|
| 320 |
Printf.eprintf "\n\nOut = %s\n\nOption is : %s\n\n" source_file !Options.dest_file; |
|
| 320 | 321 |
let source_out = open_out source_file in |
| 321 | 322 |
let fmt = formatter_of_out_channel source_out in |
| 322 | 323 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,"); |
| ... | ... | |
| 355 | 356 |
| _ -> assert false |
| 356 | 357 |
|
| 357 | 358 |
let anonymous filename = |
| 359 |
Printf.eprintf "\n\nAnonymous called with : %s\n" filename; |
|
| 358 | 360 |
let ok_ext, ext = List.fold_left |
| 359 | 361 |
(fun (ok, ext) ext' -> |
| 360 | 362 |
if not ok && Filename.check_suffix filename ext' then |
| ... | ... | |
| 373 | 375 |
Corelang.add_internal_funs (); |
| 374 | 376 |
try |
| 375 | 377 |
Printexc.record_backtrace true; |
| 376 |
Arg.parse Options.options anonymous usage |
|
| 378 |
Printf.eprintf "\nParsing\n"; |
|
| 379 |
Arg.parse Options.options anonymous usage; |
|
| 380 |
Printf.eprintf "\nDest=%s\n" !Options.dest_file |
|
| 377 | 381 |
with |
| 378 | 382 |
| Parse.Syntax_err _ | Lexer_lustre.Error _ |
| 379 | 383 |
| Types.Error (_,_) | Clocks.Error (_,_) |
Also available in: Unified diff
Arrays