let setup : unit -> any_input = fun () -> (* Formatter to write debug output to. *) (match Flags.debug_log () with (* Write to stdout by default. *) | None -> () (* Open channel to given file and create formatter on channel. *) | Some f -> let oc = try open_out f with Sys_error msg -> Format.sprintf "Could not open debug logfile \"%s\": \"%s\"" f msg |> failwith in Debug.set_formatter (Format.formatter_of_out_channel oc) ) ; (* Record backtraces on log levels debug and higher. *) if output_on_level L_debug then Printexc.record_backtrace true ; (* /!\ ================================================================== /!\ /!\ Must not use [vtalrm] signal, this is used internally by the OCaml /!\ /!\ [Threads] module. /!\ /!\ ================================================================== /!\ *) (* Raise exception on CTRL+C. *) Sys.catch_break true ; (* Set sigalrm handler. *) Signals.set_sigalrm_timeout_from_flag () ; (* Install generic signal handlers for other signals. *) Signals.set_sigint () ; Signals.set_sigpipe () ; Signals.set_sigterm () ; Signals.set_sigquit () ; (* Starting global timer. *) Stat.start_timer Stat.total_time ; let in_file = Flags.input_file () in Event.log L_info "Parsing %s." (match in_file with | "" -> "standard input" | _ -> "input file \"" ^ in_file ^ "\""); try (* in_file |> *) match Flags.input_format () with | `Lustre -> Input (InputSystem.read_input_lustre in_file) | `Native -> Input (InputSystem.read_input_native in_file) | `Horn -> Event.log L_fatal "Horn clauses are not supported." ; Event.terminate_log () ; exit ExitCodes.error with (* Could not create input system. *) | LustreAst.Parser_error -> (* Don't do anything for parser error, they should already have printed some stuff. *) Event.terminate_log () ; exit ExitCodes.error | e -> let backtrace = Printexc.get_raw_backtrace () in Event.log L_fatal "Error opening input file \"%s\":@ %s%a" (Flags.input_file ()) (Printexc.to_string e) (if Printexc.backtrace_status () then fun fmt -> Format.fprintf fmt "@\nBacktrace:@ %a" print_backtrace else fun _ _ -> ()) backtrace; (* Terminating log and exiting with error. *) Event.terminate_log () ; exit ExitCodes.error