Commit 3a867752 authored by MARCHE Claude's avatar MARCHE Claude

[jessie3] improved test output

parent 8ac813a3
......@@ -22,7 +22,7 @@ module OutputFile =
open Why3
let run_on_task prover prover_driver t =
let run_on_task fmt prover prover_driver t =
let result =
Call_provers.wait_on_call
(Why3.Driver.prove_task
......@@ -30,12 +30,9 @@ let run_on_task prover prover_driver t =
~timelimit:3
prover_driver t ()) ()
in
let p = prover.Whyconf.prover in
ACSLtoWhy3.Self.result "Status with %s %s: %a" p.Whyconf.prover_name
p.Whyconf.prover_version
Call_provers.print_prover_answer result.Call_provers.pr_answer
Format.fprintf fmt "%a" Call_provers.print_prover_answer result.Call_provers.pr_answer
let get_prover config env acc name =
let get_prover config env acc (short, name) =
let prover =
try
let fp = Whyconf.parse_filter_prover name in
......@@ -53,16 +50,21 @@ let get_prover config env acc name =
ACSLtoWhy3.Self.fatal "Failed to load driver for %s: %a@." name
Exn_printer.exn_printer e
in
(prover,driver)::acc
(short,prover,driver)::acc
let process () =
let prog = Ast.get () in
(* File.pretty_ast (); *)
let provers =
List.fold_left (get_prover ACSLtoWhy3.config ACSLtoWhy3.env) []
[ "Alt-Ergo,0.94";
"Z3,3.2"; "Z3,4.0";
"CVC3,2.2"; "CVC3,2.4.1"]
List.fold_left
(get_prover ACSLtoWhy3.config ACSLtoWhy3.env)
[]
[ "Z42", "Z3,4.2";
"Z32", "Z3,3.2";
"C24", "CVC3,2.4.1";
"C22", "CVC3,2.2";
"AlE", "Alt-Ergo,0.94";
]
in
let theories = ACSLtoWhy3.prog prog in
try
......@@ -70,10 +72,17 @@ let process () =
ACSLtoWhy3.Self.result "running theory 1:";
ACSLtoWhy3.Self.result "@[<hov 2>%a@]" Pretty.print_theory th;
let tasks = Task.split_theory th None None in
ACSLtoWhy3.Self.result "@[<h 0>%a@]"
(Pp.print_list Pp.comma
(fun fmt (_n,p,_d) ->
let p = p.Whyconf.prover in
Format.fprintf fmt "%s %s" p.Whyconf.prover_name p.Whyconf.prover_version))
provers;
let _ =
List.fold_left (fun n t ->
ACSLtoWhy3.Self.result "Dealing with task %d" n;
List.iter (fun (p,d) -> run_on_task p d t) provers;
ACSLtoWhy3.Self.result "@[<h 0>Task %d: %a@]" n
(Pp.print_list Pp.comma (fun fmt (_n,p,d) -> run_on_task fmt p d t))
provers;
n+1) 1 tasks
in ())
theories
......
......@@ -6,9 +6,18 @@
/*@ lemma test1 : 2 + 0xa == 0xc;
@*/
/*@ lemma test_ofl : 0xffffffff + 1 == 0x100000000;
@*/
/*@ lemma test2 : 0.0 + 1.1 == 1.1;
@*/
/*@ lemma test3 : 10.0 * 0.1 == 1.0;
@*/
/*@ lemma test4 : 0x1.1p4 == 17.0;
@*/
/*
Local Variables:
......
......@@ -20,12 +20,8 @@
lemma l1 : forall x:int. f1 x >= 1
end
[jessie3] Dealing with task 1
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory BagInt
(* use BuiltIn *)
......@@ -58,12 +54,8 @@
lemma l2 : f1 1 = 2
end
[jessie3] Dealing with task 1
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations1
(* use BuiltIn *)
......@@ -76,12 +68,8 @@
lemma union_comm : forall b1:bag, b2:bag. bag_union b1 b2 = bag_union b2 b1
end
[jessie3] Dealing with task 1
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Unknown
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Task 1: Unknown, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
......@@ -98,3 +86,4 @@
(* use Global_logic_declarations1 *)
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[kernel] preprocessing with "gcc -C -E -I. tests/basic/constants.c"
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] found 5 logic decl(s)
[jessie3] made 1 theory(ies)
[jessie3] made 0 function(s)
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations
(* use BuiltIn *)
(* use int.Int *)
(* use real.Real *)
lemma test1 : (2 + 0xa) = 0xc
lemma test_ofl : (0xffffffff + 1) = 0x100000000
lemma test2 : (0.0 + 1.1) = 1.1
lemma test3 : (10.0 * 0.1) = 1.0
lemma test4 : 0x1.1p4 = 17.0
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 3: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 4: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 5: Valid, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
(* use Bool *)
(* use Unit *)
(* use Prelude *)
(* use int.Int *)
(* use real.Real *)
(* use Global_logic_declarations *)
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
......@@ -3,6 +3,16 @@
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] processing function f
[jessie3] processing function g
[kernel] Plug-in jessie3 aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
'[Plug-in jessie3] instr Set'.
[kernel] The full backtrace is:
Called from file "register.ml", line 69, characters 17-37
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
Called from file "src/kernel/cmdline.ml", line 720, characters 2-9
Called from file "src/kernel/cmdline.ml", line 197, characters 4-8
Unexpected error (Invalid_argument("Mlw.vty_arrow")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Oxygen-20120901.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
......@@ -23,6 +23,7 @@
function bag_union (bag 'x) (bag 'x) : bag 'x
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
......@@ -39,3 +40,4 @@
(* use Bag *)
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
......@@ -2,6 +2,16 @@
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] processing function f
[kernel] Plug-in jessie3 aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
'[Plug-in jessie3] instr Set'.
[kernel] The full backtrace is:
Called from file "register.ml", line 69, characters 17-37
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
Called from file "src/kernel/cmdline.ml", line 720, characters 2-9
Called from file "src/kernel/cmdline.ml", line 197, characters 4-8
Unexpected error (Invalid_argument("Mlw.vty_arrow")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Oxygen-20120901.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
......@@ -3,6 +3,16 @@
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] creating logic symbol 739 (sqr)
[jessie3] processing function isqrt
[kernel] Plug-in jessie3 aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
'[Plug-in jessie3] stmt Loop'.
[kernel] The full backtrace is:
Called from file "register.ml", line 69, characters 17-37
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
Called from file "src/kernel/cmdline.ml", line 720, characters 2-9
Called from file "src/kernel/cmdline.ml", line 197, characters 4-8
Unexpected error (Invalid_argument("Mlw.vty_arrow")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Oxygen-20120901.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
......@@ -26,48 +26,14 @@
lemma test4r : forall x:real, y:real. (x - y) = (- (y - x))
end
[jessie3] Dealing with task 1
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] Dealing with task 2
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] Dealing with task 3
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] Dealing with task 4
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] Dealing with task 5
[jessie3] Status with CVC3 2.4.1: Unknown
[jessie3] Status with CVC3 2.2: Unknown
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] Dealing with task 6
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] Dealing with task 7
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 3: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 4: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 5: Valid, Unknown, Unknown, Valid, Valid
[jessie3] Task 6: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 7: Valid, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
......@@ -84,3 +50,4 @@
(* use Global_logic_declarations *)
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
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