let main () = (* Set everything up and produce input system. *) let Input input_sys = setup () in (* Notify user of silent contract loading. *) (try InputSystem.silent_contracts_of input_sys |> List.iter ( function | (_, []) -> () | (scope,contracts) -> Event.log L_note "Silent contract%s loaded for system %a: @[<v>%a@]" (if 1 < List.length contracts then "s" else "") Scope.pp_print_scope scope (pp_print_list Format.pp_print_string "@ ") contracts ) with (InputSystem.UnsupportedFileFormat ff) -> Event.log L_warn "Loading of silent contracts is not supported for %s files" ff ); (* Not launching if we're just translating contracts. *) match Flags.Contracts.translate_contracts () with | Some target -> ( let src = Flags.input_file () in Event.log_uncond "Translating contracts to file \"%s\"" target ; try ( InputSystem.translate_contracts_lustre src target ; Event.log_uncond "Success" ) with e -> Event.log L_error "Could not translate contracts from file \"%s\":@ %s" src (Printexc.to_string e) ) | None -> try Kind2Flow.run input_sys with e -> ( Event.log L_fatal "Caught unexpected exception: %s" (Printexc.to_string e) ; Event.terminate_log () ; exit ExitCodes.error )