Commit 3ffc4e0a authored by Sylvain Dailler's avatar Sylvain Dailler

TODO amend: activate coverage tool

To see coverage:
- compile (you have to manually copy mlmpfr_dummy to mlmpfr_wrapper)
- launch why3prove or other on files (careful a lot of bisetc*.out will
appear everywhere in your folder)
- bisect-ppx-report -ignore-missing-files -html coverage -I . bisect*.out
- firefox coverage/index.html

One linking problem with menhir remains: I had to remove the code that
extract user locations in src/util/loc.ml
Also plugins test have been disabled.
parent 89af91b5
......@@ -302,7 +302,7 @@ goods stdlib/mach
echo ""
echo "=== Checking drivers ==="
drivers drivers
#drivers drivers
echo ""
echo "=== Checking bad files ==="
......@@ -339,8 +339,8 @@ goods examples/in_progress/ring_decision "-L examples/in_progress/ring_decision"
goods examples/multiprecision "-L examples/multiprecision"
goods examples/prover "-L examples/prover --debug ignore_unused_vars"
goods examples/in_progress
plugins tests/python --type-only py
plugins tests/microc --type-only c
# plugins tests/python --type-only py
# plugins tests/microc --type-only c
echo ""
echo "=== Checking valid goals ==="
......
......@@ -77,7 +77,7 @@ run () {
echo "Strongest Postcondition" > "$f.out"
printf "Strongest Postcondition ${file_path} ($1)... "
fi
$dir/../bin/why3prove.opt --json --debug print_model_attrs${wp_sp} -P "$1,counterexamples" --timelimit 1 -a split_vc "${file_path}.mlw" | \
$dir/../bin/why3prove --json --debug print_model_attrs${wp_sp} -P "$1,counterexamples" --timelimit 1 -a split_vc "${file_path}.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
......
......@@ -55,7 +55,7 @@ run_dir () {
for f in $LIST; do
d=`dirname $f`
printf "Replaying $d ... "
if ../bin/why3replay.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP ; then
if ../bin/why3replay -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP ; then
printf "OK"
cat $TMP $TMPERR
success=`expr $success + 1`
......
......@@ -5,6 +5,7 @@
ident ty term pattern decl coercion theory
task pretty dterm env trans printer model_parser
)
(preprocess (pps bisect_ppx))
(flags -open Why3_util -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util num)
)
......@@ -12,5 +12,6 @@
parse_smtv2_model
)
(flags -open Why3_util -open Why3_core -w A-4-9-41-44-45-50-52@5@8@48)
(preprocess (pps bisect_ppx))
(libraries why3.util why3.core num unix)
)
......@@ -8,6 +8,7 @@
)
)
(flags -open Why3.V1 -linkall)
(preprocess (pps bisect_ppx))
(package why3-ide)
)
......@@ -15,6 +16,8 @@
(name why3_resetgc)
(modules why3_resetgc)
(c_names resetgc)
(preprocess (pps bisect_ppx))
)
(executable
......@@ -23,5 +26,6 @@
(modules wserver why3web)
(libraries why3)
(flags -open Why3.V1 -linkall)
(preprocess (pps bisect_ppx))
(package why3)
)
......@@ -2,10 +2,11 @@
(name why3_mlw)
(public_name why3.mlw)
(modules
ity expr pdecl eval_match typeinv vc pmodule dexpr
ity expr pdecl eval_match typeinv vc pmodule dexpr big_real
pinterp mltree compile mlinterp pdriver cprinter ml_printer
ocaml_printer cakeml_printer
)
(preprocess (pps bisect_ppx))
(flags -open Why3_util -open Why3_core -open Why3_driver -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.driver num unix)
)
......@@ -9,6 +9,7 @@
(modules
ptree glob typing parser typing lexer
)
(preprocess (pps bisect_ppx))
(flags -open Why3_util -open Why3_core -open Why3_mlw -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.mlw num menhirLib)
)
......@@ -6,6 +6,7 @@
pvs isabelle
simplify gappa cvc3 yices mathematica
)
(preprocess (pps bisect_ppx))
(flags -open Why3_util -open Why3_core -open Why3_transform -open Why3_mlw -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.transform why3.mlw num)
)
......@@ -14,6 +14,7 @@
(zip -> compress_z.ml)
( -> compress_none.ml))
)
(preprocess (pps bisect_ppx))
(flags -open Why3_util -open Why3_core -open Why3_transform -open Why3_driver -open Why3_parser -w A-4-9-41-44-45-50-52@5@8@48)
)
......
......@@ -4,6 +4,7 @@
(modules why3config why3execute why3extract why3prove why3realize why3wc)
(flags -linkall -open Why3.V1)
(package why3)
(preprocess (pps bisect_ppx))
)
(executable
......@@ -12,6 +13,7 @@
(libraries why3)
(modules main)
(flags -linkall -open Why3.V1)
(preprocess (pps bisect_ppx))
(package why3)
)
......@@ -22,6 +24,7 @@
(name why3_unix_scheduler)
(modules unix_scheduler)
(libraries why3)
(preprocess (pps bisect_ppx))
(flags -linkall -open Why3.V1)
)
......@@ -30,6 +33,7 @@
(libraries why3 why3_unix_scheduler)
(modules why3replay)
(flags -linkall -open Why3.V1 -open Why3_unix_scheduler)
(preprocess (pps bisect_ppx))
(package why3)
)
......@@ -38,5 +42,6 @@
(modules why3shell)
(libraries why3 why3_unix_scheduler)
(flags -linkall -open Why3.V1 -open Why3_unix_scheduler)
(preprocess (pps bisect_ppx))
(package why3)
)
......@@ -21,6 +21,7 @@
intro_vc_vars_counterexmp prepare_for_counterexmp
induction induction_pr matching reflection
)
(preprocess (pps bisect_ppx))
(flags -open Why3_util -open Why3_core -open Why3_mlw -open Why3_parser -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.mlw why3.parser num)
)
......@@ -10,8 +10,9 @@
hashcons wstdlib exn_printer
json_base json_parser json_lexer
debug loc lexlib print_tree
cmdline warning sysutil rc plugin bigInt number vector pqueue
cmdline warning sysutil rc plugin bigInt number vector pqueue mlmpfr_wrapper
)
(preprocess (pps bisect_ppx))
(flags -w A-4-9-41-44-45-50-52@5@8@48)
(libraries num dynlink str unix)
(libraries num dynlink str unix menhirLib)
)
......@@ -54,11 +54,12 @@ let join (f1,l1,b1,e1) (f2,_,b2,e2) =
assert (f1 = f2); (f1,l1,b1,e1+e2-b2)
let extract (b,e) =
let f = b.pos_fname in
(*let f = b.pos_fname in
let l = b.pos_lnum in
let fc = b.pos_cnum - b.pos_bol in
let lc = e.pos_cnum - b.pos_bol in
(f,l,fc,lc)
(f,l,fc,lc)*)
("", 1, 1, 1)
let compare = Pervasives.compare
let equal = Pervasives.(=)
......
......@@ -6,5 +6,6 @@
why3session_main)
(libraries why3)
(flags -open Why3.V1 -linkall)
(preprocess (pps bisect_ppx))
(package why3)
)
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