Commit bed36a37 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add some extraction tests to the bench.

parent c0758c6b
......@@ -159,6 +159,26 @@ execute () {
fi
}
extract () {
pgm="bin/why3extract$suffix"
dir=$1
shift
for f in $dir/*.mlw; do
printf " $f... "
if ($pgm $@ $f -o bench_test.ml && ocaml -noinit bench_test.ml) > /dev/null 2> /dev/null; then
echo "ok"
else
echo "extract test failed!"
echo $pgm $@ $f
$pgm $@ $f -o bench_test.ml
ocaml -noinit bench_test.ml
rm -f bench_test.ml
exit 1
fi
done
rm -f bench_test.ml
}
extract_and_run () {
dir=$1
shift
......@@ -349,6 +369,7 @@ execute examples/vstte10_queens.mlw NQueens.test8
echo ""
echo "=== Checking extraction to OCaml ==="
extract bench/extraction -D ocaml64
extract_and_run examples/euler001 euler001.ml 1000000
extract_and_run examples/gcd gcd.ml 6 15
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
......
......@@ -5,7 +5,3 @@ let g (_:unit) = ()
let good = f (fun x -> g x)
let bad = f g
let ugly = g
let main () = ugly ()
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