Commit 95b2438a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix compilation of Jessie 3.

parent 6662cff8
......@@ -27,7 +27,7 @@ Jessie3.cmx: $(addsuffix .cmx, $(MODULES))
ocamlopt.opt $(FLAGS) $(INCLUDE) -o $@ -pack $^
Jessie3.cmxs: Jessie3.cmx
ocamlopt.opt -shared $(FLAGS) $(INCLUDE) -o $@ $(addsuffix .cmx, @MENHIRLIB@) $(addsuffix .cmxa, @ZIPLIB@) $(WHYLIB)/why3.cmxa $^
ocamlopt.opt -shared $(FLAGS) $(INCLUDE) -o $@ nums.cmxa $(addsuffix .cmx, @MENHIRLIB@) $(addsuffix .cmxa, @ZIPLIB@) $(WHYLIB)/why3.cmxa $^
%.cmo: %.ml
ocamlc.opt $(FLAGS) $(INCLUDE) -c $^
......
......@@ -27,12 +27,13 @@ let () = Debug.set_flag Call_provers.debug
*)
let run_on_task fmt prover prover_driver t =
let limit = { Call_provers.empty_limit with Call_provers.limit_time = 3 } in
let result =
Call_provers.wait_on_call
(Why3.Driver.prove_task
~command:prover.Whyconf.command
~timelimit:3
prover_driver t ()) ()
~limit
prover_driver t)
in
Format.fprintf fmt "%a" Call_provers.print_prover_answer result.Call_provers.pr_answer;
match result.Call_provers.pr_answer with
......@@ -53,7 +54,7 @@ let get_prover config env acc (short, name) =
(* loading the driver *)
let driver : Why3.Driver.driver =
try
Why3.Driver.load_driver env prover.Whyconf.driver []
Why3.Whyconf.load_driver (Why3.Whyconf.get_main config) env prover.Whyconf.driver []
with e ->
ACSLtoWhy3.Self.fatal "Failed to load driver for %s: %a@." name
Exn_printer.exn_printer e
......
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