Commit 748e9b4c authored by MARCHE Claude's avatar MARCHE Claude

jessie3: fixing tests in progress

parent 2aaff9ae
......@@ -8,11 +8,10 @@ WHYLIB = ../../lib/why3
INCLUDE = -I $(FRAMAC_LIBDIR) -I $(FRAMAC_LIBDIR)/plugins -I +ocamlgraph @ZIPINCLUDE@ @MENHIRINCLUDE@ -I $(WHYLIB)
FLAGS = -w +a-3-4-6-9-41-44-45-48 -annot -bin-annot -g
all: Jessie3.cma
OCAMLLEX = @OCAMLLEX@
all:: Jessie3.cma Jessie3.cmxs
Makefile: Makefile.in ../../config.status
(cd ../../ ; ./config.status chmod --file src/jessie/Makefile)
......@@ -41,6 +40,7 @@ test.opt:
frama-c -kernel-debug 2 -load-module ./Jessie3.cmxs -jessie3 tests/basic/forty-two.c
tests::
time -p ptests.opt
grep 'Task\|Ergo' tests/basic/result/*.res.log tests/demo/result/*.res.log
......
......@@ -22,6 +22,8 @@ module OutputFile =
open Why3
let () = Debug.set_flag Call_provers.debug
let run_on_task fmt prover prover_driver t =
let result =
Call_provers.wait_on_call
......@@ -30,7 +32,11 @@ let run_on_task fmt prover prover_driver t =
~timelimit:3
prover_driver t ()) ()
in
Format.fprintf fmt "%a" Call_provers.print_prover_answer result.Call_provers.pr_answer
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
| _ -> ()
let get_prover config env acc (short, name) =
let prover =
......
[kernel] preprocessing with "gcc -C -E -I. tests/basic/app.c"
[jessie3] creating logic symbol 739 (f)
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/basic/app.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] creating logic symbol 68 (f)
[jessie3] processing function g
[jessie3] created program function g (740)
[jessie3] created program function g (69)
[jessie3] found 1 logic decl(s)
[jessie3] made 1 theory(ies)
[jessie3] made 1 function(s)
[jessie3] Running provers...
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations
(* use why3.BuiltIn *)
(* use why3.BuiltIn.BuiltIn *)
(* use int.Int *)
......@@ -17,16 +25,16 @@
function f (x:int) : int = x + 1
end
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
(* use why3.BuiltIn.BuiltIn *)
(* use why3.Bool *)
(* use why3.Bool.Bool *)
(* use why3.Unit *)
(* use why3.Unit.Unit *)
(* use why3.Prelude *)
(* use why3.Prelude.Prelude *)
(* use int.Int *)
......@@ -38,9 +46,9 @@
(* use ref.Ref *)
(* use mach_int.Int32 *)
(* use mach.int.Int32 *)
goal WP_parameter_g : true
end
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter g): Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter g): Valid, Valid, Valid, Valid, Valid
......@@ -2,7 +2,8 @@
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] preprocessing with "gcc -C -E -I. tests/basic/constants.c"
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/basic/constants.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] found 5 logic decl(s)
......
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