Commit 4d888158 authored by Maximilien Colange's avatar Maximilien Colange

Proper error handling.

parent 4fcfe085
......@@ -68,17 +68,7 @@ let main() =
Printexc.record_backtrace true;
Arg.parse_dynamic arg_list set_command usage;
let module MC = (val !mc_module : OPTIONS) in
if ( !tafile = "" ) then
(
Arg.usage [] usage;
exit 1
);
if ( !qfile = "" ) then
(
qfile := (Filename.chop_suffix !tafile ".xml") ^ ".q";
(* Log.warningf "Guessing query file: %s\n" !qfile *)
);
let res = Options.verify (module MC) !tafile !qfile in
let res = Options.verify (module MC) in
Printf.printf "Result of verification is %s\n" res;
if (!show_gc_stats) then
Gc.print_stat stdout
......
......@@ -275,11 +275,19 @@ let ofile = ref ""
let load () =
match !inputtype with
| XML -> assert(!tafile <> ""); Ita.loadedmodule := Some (module Uppaalta.GenericUAutomaton(struct let tafile = !tafile;; let qfile = !qfile end))
| CMXS -> assert(!ofile <> ""); Dynlink.loadfile !ofile; assert(!Ita.loadedmodule <> None)
| CMXS ->
begin
assert(!ofile <> "");
try
Dynlink.loadfile !ofile;
with
| Dynlink.Error e -> failwith (Dynlink.error_message e)
end;
assert(!Ita.loadedmodule <> None)
| _ -> failwith "unsupported input format"
let verify (module O : OPTIONS) tafile qfile =
let verify (module O : OPTIONS) =
load ();
let module TA = (val (O.get_ta ())) in
let ta = TA.model in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment