Project

General

Profile

« Previous | Next » 

Revision 84902260

Added by jbraine almost 6 years ago

Arrays

View differences:

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