Commit c73a3aa3 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Merge branch 'new_ide'

parents 2d6e7027 b4a7d369
.git
\ No newline at end of file
.git
......@@ -78,12 +78,8 @@ opam:
deploy:
stage: deploy
script:
- autoconf && (automake --add-missing 2> /dev/null || true)
- docker build -t bench-image -f misc/Dockerfile.init .
- docker build -t deploy-image -f misc/Dockerfile.deploy .
- docker login -u gitlab-ci-token -p $CI_JOB_TOKEN $CI_REGISTRY
- docker tag deploy-image $CI_REGISTRY_IMAGE:$CI_COMMIT_REF_SLUG
- docker push $CI_REGISTRY_IMAGE:$CI_COMMIT_REF_SLUG
- docker image prune -f
- misc/ci-deploy.sh
only:
- master
- /^bugfix[/]v[0-9.]*$/
- tags
......@@ -8,7 +8,13 @@ files=""
while test $# != 0; do
case "$1" in
"-update-oracle")
updateoracle=true;;
updateoracle=true;;
"-"*)
printf "unknown option: %s\n" "$1"
printf "usage: ce-bench [-update-oracle] <files>\n"
printf " <files> must be given without the '.mlw' suffix\n"
printf " if <files> empty, use all files from directory 'ce'\n"
exit 2;;
*)
files="$files $1"
esac
......@@ -16,20 +22,19 @@ shift
done
if test "$files" = "" ; then
files="ce/*.mlw"
files="$dir/ce/*.mlw"
fi
cd $dir
# $1 = prover, $2 = file
run () {
printf " $2 ($1)... "
f="$2_$1"
../bin/why3prove.opt -P "$1" --timelimit 1 -a split_intros_goal_wp --get-ce "$2.mlw" | \
$dir/../bin/why3prove.opt -P "$1" --timelimit 1 -a split_intros_goal_wp --get-ce "$2.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)//' > "$f.out"
../bin/why3prove.opt -P "$1" --timelimit 1 -a split_intros_goal_wp --get-ce "$2.mlw" | \
$dir/../bin/why3prove.opt -P "$1" --timelimit 1 -a split_intros_goal_wp --get-ce "$2.mlw" | \
sed 's/ ([0-9]\+\.[0-9]\+s)//' >> "$f.out"
if cmp "$f.oracle" "$f.out" > /dev/null 2>&1 ; then
echo "ok"
......@@ -48,8 +53,10 @@ run () {
for file in $files; do
filedir=`dirname $file`
filebase=`basename $file .mlw`
run CVC4,1.5 ce/$filebase
run Z3,4.5.0 ce/$filebase
run Z3,4.6.0 ce/$filebase
printf "Running provers on $filedir/$filebase.mlw\n";
run CVC4,1.5 $filedir/$filebase
run Z3,4.5.0 $filedir/$filebase
run Z3,4.6.0 $filedir/$filebase
done
ce/algebraic_type.mlw M G: Unknown (other)
ce/algebraic_type.mlw M G: Unknown (other)
bench/ce/algebraic_type.mlw M G: Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G: Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_type.mlw M G: Unknown (other)
ce/algebraic_type.mlw M G: Unknown (other)
bench/ce/algebraic_type.mlw M G: Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G: Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_type.mlw M G: Unknown (other)
ce/algebraic_type.mlw M G: Unknown (other)
bench/ce/algebraic_type.mlw M G: Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G: Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -6,7 +6,7 @@ Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -14,7 +14,7 @@ Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -22,7 +22,7 @@ Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -30,7 +30,7 @@ Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -38,7 +38,7 @@ Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -46,7 +46,7 @@ Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -54,7 +54,7 @@ Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -62,7 +62,7 @@ Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -70,7 +70,7 @@ Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -78,7 +78,7 @@ Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -86,7 +86,7 @@ Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -94,7 +94,7 @@ Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "0" }
......@@ -102,7 +102,7 @@ Line 31:
i = {"type" : "Integer" ,
"val" : "0" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "0" }
......@@ -110,7 +110,7 @@ Line 25:
old i = {"type" : "Integer" ,
"val" : "0" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -118,7 +118,7 @@ Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -126,7 +126,7 @@ Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -134,7 +134,7 @@ Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -142,7 +142,7 @@ Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -150,7 +150,7 @@ Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -158,7 +158,7 @@ Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -166,7 +166,7 @@ Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -174,7 +174,7 @@ Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -182,7 +182,7 @@ Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -190,7 +190,7 @@ Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -198,7 +198,7 @@ Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
......@@ -206,7 +206,7 @@ Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "0" }
......@@ -214,7 +214,7 @@ Line 31:
i = {"type" : "Integer" ,
"val" : "0" }
ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "0" }
......
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records VC var_overwrite: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-176" }
Line 31:
i = {"type" : "Integer" ,
"val" : "-176" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "2" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "2" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)