Commit b424b944 authored by MARCHE Claude's avatar MARCHE Claude

jessie3 oracles

parent 04eed327
......@@ -34,10 +34,12 @@ Jessie3.cmxs: Jessie3.cmx
ocamlopt.opt $(FLAGS) $(INCLUDE) -for-pack Jessie3 -c $^
test.byte:
frama-c.byte -kernel-debug 2 -load-module ./Jessie3.cma -jessie3 tests/basic/forty-two.c
frama-c.byte -load-module ./Jessie3.cma -jessie3 tests/basic/forty-two.c
# -kernel-debug 2
test.opt:
frama-c -kernel-debug 2 -load-module ./Jessie3.cmxs -jessie3 tests/basic/forty-two.c
frama-c -load-module ./Jessie3.cmxs -jessie3 tests/basic/forty-two.c
# -kernel-debug 2
tests::
time -p ptests.opt
......
......@@ -22,7 +22,9 @@ module OutputFile =
open Why3
(*
let () = Debug.set_flag Call_provers.debug
*)
let run_on_task fmt prover prover_driver t =
let result =
......@@ -35,7 +37,7 @@ let run_on_task fmt prover prover_driver t =
Format.fprintf fmt "%a" Call_provers.print_prover_answer result.Call_provers.pr_answer;
match result.Call_provers.pr_answer with
| Call_provers.Failure _ | Call_provers.HighFailure ->
Format.fprintf fmt "@\n=======@\n%s@\n======@\n" result.Call_provers.pr_output
Format.fprintf fmt "@\n=======@\n%s@\n======@\n" result.Call_provers.pr_output
| _ -> ()
let get_prover config env acc (short, name) =
......
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