Commit 24e35c79 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'next' into new_ide

# Conflicts:
#	examples/logic/einstein/why3session.xml
#	examples/tests-provers/div/why3session.xml
#	src/driver/whyconf.ml
parents dd2493a7 c89bcbd7
:x: marks a potential source of incompatibility
Provers
* support for Alt-Ergo 2.0.0 (released Nov 14, 2017)
* support for Z3 4.6.0 (released Dec 18, 2017)
Standard library
* fix compatibility of theory int.Exponentiation with instances
where multiplication is not commutative.
fix corresponding realizations in Coq and Isabelle/HOL :x:
Bug fixes
* Fix issue #50:
share/Makefile.config is missing when enable_relocation=yes
Version 0.88.2, December 7, 2017
--------------------------------
......
theory T
goal g : forall x:int. x = (at x 'L)
end
......@@ -2,72 +2,105 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="2.19" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Spass" version="3.7" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="7" name="Yices" version="1.0.38" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="8" name="Metis" version="2.3" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="3.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="10" name="Eprover" version="1.8-001" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="11" name="Alt-Ergo" version="0.95.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="12" name="Alt-Ergo" version="1.20.prv" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="13" name="CVC4" version="1.3" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="14" name="Vampire" version="0.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="15" name="Alt-Ergo" version="1.00.prv" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="16" name="veriT" version="201410" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="17" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="18" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="19" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../einstein.why">
<theory name="Bijection" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
<prover id="17" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="18" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="19" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="20" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="21" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../einstein.why" expanded="true">
<theory name="Bijection" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Einstein" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Einstein" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Goals" sum="9fe1211e777a560b454f17977bc1a636">
<goal name="G1" proved="true">
<theory name="Goals" sum="9fe1211e777a560b454f17977bc1a636" expanded="true">
<goal name="G1" expl="" expanded="true">
<proof prover="0"><result status="timeout" time="2.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="unknown" time="0.17"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="5" obsolete="true"><result status="timeout" time="0.99"/></proof>
<proof prover="7" obsolete="true"><result status="unknown" time="0.00"/></proof>
<proof prover="8" obsolete="true"><result status="unknown" time="0.89"/></proof>
<proof prover="4"><result status="valid" time="0.88"/></proof>
<proof prover="5"><result status="timeout" time="0.99"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="unknown" time="0.89"/></proof>
<proof prover="9"><result status="valid" time="0.26"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="10"><result status="timeout" time="2.00"/></proof>
<proof prover="11"><result status="timeout" time="2.00"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.50"/></proof>
<proof prover="15"><result status="timeout" time="2.00"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="timeout" time="1.01"/></proof>
<proof prover="18"><result status="valid" time="0.17"/></proof>
<proof prover="19"><result status="valid" time="0.06"/></proof>
<proof prover="17"><result status="valid" time="1.17" steps="983"/></proof>
<proof prover="18"><result status="valid" time="1.41" steps="989"/></proof>
<proof prover="19"><result status="valid" time="0.21"/></proof>
<proof prover="20"><result status="valid" time="0.21"/></proof>
<proof prover="21"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="Wrong">
<goal name="Wrong" expl="" expanded="true">
<proof prover="0"><result status="timeout" time="2.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="unknown" time="0.06"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="5" obsolete="true"><result status="timeout" time="0.99"/></proof>
<proof prover="7" obsolete="true"><result status="unknown" time="0.00"/></proof>
<proof prover="8" obsolete="true"><result status="unknown" time="0.93"/></proof>
<proof prover="5"><result status="timeout" time="0.99"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="unknown" time="0.93"/></proof>
<proof prover="9"><result status="timeout" time="1.00"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="14"><result status="unknown" time="2.00"/></proof>
<proof prover="11"><result status="timeout" time="2.00"/></proof>
<proof prover="12"><result status="timeout" time="1.01"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="unknown" time="1.00"/></proof>
<proof prover="15"><result status="unknown" time="1.33"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="unknown" time="0.59"/></proof>
<proof prover="18"><result status="timeout" time="1.00"/></proof>
<proof prover="19"><result status="unknown" time="0.06"/></proof>
<proof prover="17"><result status="unknown" time="0.57"/></proof>
<proof prover="18"><result status="unknown" time="0.66"/></proof>
<proof prover="19"><result status="timeout" time="1.00"/></proof>
<proof prover="20"><result status="timeout" time="1.00"/></proof>
<proof prover="21"><result status="unknown" time="0.07"/></proof>
</goal>
<goal name="G2" proved="true">
<goal name="G2" expl="" expanded="true">
<proof prover="0"><result status="timeout" time="1.99"/></proof>
<proof prover="1"><result status="timeout" time="2.00"/></proof>
<proof prover="2"><result status="unknown" time="0.06"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.76"/></proof>
<proof prover="5" obsolete="true"><result status="timeout" time="0.99"/></proof>
<proof prover="7" obsolete="true"><result status="unknown" time="0.00"/></proof>
<proof prover="8" obsolete="true"><result status="unknown" time="1.85"/></proof>
<proof prover="4"><result status="timeout" time="2.00"/></proof>
<proof prover="5"><result status="timeout" time="0.99"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="unknown" time="1.85"/></proof>
<proof prover="9"><result status="valid" time="0.62"/></proof>
<proof prover="10"><result status="valid" time="0.79"/></proof>
<proof prover="11"><result status="timeout" time="2.00"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.27"/></proof>
<proof prover="15"><result status="valid" time="1.82" steps="523"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="valid" time="0.84" steps="1151"/></proof>
<proof prover="18"><result status="valid" time="0.13"/></proof>
<proof prover="19"><result status="valid" time="0.06"/></proof>
<proof prover="17"><result status="valid" time="0.78" steps="1152"/></proof>
<proof prover="18"><result status="valid" time="0.95" steps="1156"/></proof>
<proof prover="19"><result status="valid" time="0.20"/></proof>
<proof prover="20"><result status="valid" time="0.18"/></proof>
<proof prover="21"><result status="valid" time="0.05"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,6 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.2" timelimit="60" steplimit="1" memlimit="1000"/>
<prover id="2" name="Zenon" version="0.8.0" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="0"/>
......@@ -34,9 +35,11 @@
<prover id="30" name="Isabelle" version="2016-1" timelimit="100" steplimit="1" memlimit="1000"/>
<prover id="31" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="32" name="Coq" version="8.6.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="33" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../genealogy.why" expanded="true">
<theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true">
<goal name="Child_is_son_or_daughter" expanded="true">
<goal name="Child_is_son_or_daughter" expl="" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -65,8 +68,10 @@
<proof prover="30" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="21.67"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.51"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Sibling_sym" expanded="true">
<goal name="Sibling_sym" expl="" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -95,8 +100,10 @@
<proof prover="29"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Sibling_sym_1.xml"><result status="valid" time="21.58"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Sibling_is_brother_or_sister" expanded="true">
<goal name="Sibling_is_brother_or_sister" expl="" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -123,8 +130,10 @@
<proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="22.73"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Grandparent_is_grandfather_or_grandmother" expanded="true">
<goal name="Grandparent_is_grandfather_or_grandmother" expl="" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="28"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
......@@ -152,8 +161,10 @@
<proof prover="29"><result status="valid" time="0.00" steps="36"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="24.37"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="33"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Grandfather_male" expanded="true">
<goal name="Grandfather_male" expl="" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -181,8 +192,10 @@
<proof prover="28"><result status="valid" time="0.00"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Grandmother_female" expanded="true">
<goal name="Grandmother_female" expl="" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -210,8 +223,10 @@
<proof prover="28"><result status="valid" time="0.00"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="33"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Only_two_grandfathers" expanded="true">
<goal name="Only_two_grandfathers" expl="" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
......@@ -239,6 +254,7 @@
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
</file>
......
......@@ -128,9 +128,11 @@ else
echo "Counterexample regression tests succeeded. " >> $REPORT
fi
# check realizations
misc/check-realizations.sh >> $REPORT
# replay proofs
examples/regtests.sh --check-realizations &> $OUT
examples/regtests.sh &> $OUT
if test "$?" != "0" ; then
SUBJECT="$SUBJECT failed"
echo "Proof replay failed" >> $REPORT
......@@ -144,9 +146,9 @@ cp $OUT $REPORTDIR/regtests-$DATE
echo "Ending time (UTC): "`date --utc +%H:%M` >> $REPORT
# 3-line summary + 4 lines check realizations
# 3-line summary
echo "" >> $REPORT
tail -7 $OUT >> $REPORT
tail -3 $OUT >> $REPORT
echo "" >> $REPORT
# output the diff against previous run
......
......@@ -2,10 +2,6 @@
# regression tests for why3
REPLAYOPT=""
# Test realization too
CHECK_REALIZATION=""
# Don't test the rest of examples, only the realizations
ONLY_REALIZATION=""
while test $# != 0; do
case "$1" in
......@@ -19,13 +15,6 @@ case "$1" in
REPLAYOPT="$REPLAYOPT --prover $2"
shift
;;
"--check-realizations")
CHECK_REALIZATION="true"
;;
"--only-realizations")
ONLY_REALIZATION="true"
CHECK_REALIZATION="true"
;;
*)
echo "$0: Unknown option '$1'"
exit 2
......@@ -35,7 +24,6 @@ done
TMP=$PWD/why3regtests.out
TMPERR=$PWD/why3regtests.err
TMPREAL=$(mktemp -d /tmp/why3realizations-XXXXXXX)
# Current directory is /examples
cd `dirname $0`
......@@ -49,41 +37,6 @@ export total=0
export sessions=""
export shapes=""
test_generated () {
# Current directory is /why3
mkdir -p $TMPREAL/lib
echo "Testing isabelle realizations"
# First copy current realizations in a tmp directory
cp -r ../lib/isabelle/ $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' -x '*~' -x '*.aux' ../lib/isabelle $TMPREAL/lib/isabelle`
if test "$TMPDIFF" = "" ; then
printf "Isabelle realizations OK\n"
else
printf "ISABELLE REALIZATIONS FAILED, please regenerate and prove them\n"
printf "$TMPDIFF\n"
printf "Generated realizations are in /tmp. Use --only-realizations to only test realizations\n"
res=1
fi
echo "Testing coq realizations"
# First copy current realizations in a tmp directory
cp -r ../lib/coq/ $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_COQ="$TMPREAL/lib/coq" update-coq > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' -x '*~' -x '*.aux' ../lib/coq $TMPREAL/lib/coq`
if test "$TMPDIFF" = "" ; then
printf "Coq realizations OK\n"
else
printf "COQ REALIZATIONS FAILED, please regenerate and prove it\n"
printf "$TMPDIFF\n"
printf "Generated realizations are in /tmp. Use --only-realizations to only test realizations\n"
res=1
fi
}
run_dir () {
for f in `ls $1/*/why3session.xml`; do
......@@ -112,48 +65,42 @@ run_dir () {
shapes="$shapes $1/*/why3shapes.*"
}
if test "$ONLY_REALIZATION" = "" ; then
echo "=== Standard Library ==="
run_dir stdlib
echo ""
echo "=== Tests ==="
# there's no session there...
# run_dir tests
run_dir tests-provers
echo ""
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""
echo "=== BTS ==="
run_dir bts
echo ""
echo "=== Logic ==="
run_dir logic
run_dir bitvectors "-L bitvectors"
echo ""
echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir WP_revisited
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir avl "-L avl"
run_dir double_wp "-L double_wp"
run_dir prover "-L prover"
echo ""
echo "Summary : $success/$total"
echo "Sessions size : "`wc -cl $sessions | tail -1`
echo "Shapes size : "`wc -cl $shapes | tail -1`
echo "=== Standard Library ==="
run_dir stdlib
echo ""
echo "=== Tests ==="
# there's no session there...
# run_dir tests
run_dir tests-provers
echo ""
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""
echo "=== BTS ==="
run_dir bts
echo ""
echo "=== Logic ==="
run_dir logic
run_dir bitvectors "-L bitvectors"
echo ""
echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir WP_revisited
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir avl "-L avl"
run_dir double_wp "-L double_wp"
run_dir prover "-L prover"
echo ""
echo "Summary : $success/$total"
echo "Sessions size : "`wc -cl $sessions | tail -1`
echo "Shapes size : "`wc -cl $shapes | tail -1`
fi
if test "$CHECK_REALIZATION" = "true" ; then
test_generated
fi
exit $res
This diff is collapsed.
# cd to the directory of this script
cd `dirname $0`
# temporary directory where we generate realizations
TMPREAL=$(mktemp -d /tmp/why3realizations-XXXXXXX)
mkdir -p $TMPREAL/lib
echo "Testing isabelle realizations"
# First copy current realizations in a tmp directory
cp -r ../lib/isabelle/ $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' -x '*~' -x '*.aux' ../lib/isabelle $TMPREAL/lib/isabelle`
if test "$TMPDIFF" = "" ; then
printf "Isabelle realizations OK\n"
else
printf "ISABELLE REALIZATIONS FAILED, please regenerate and prove them\n"
printf "$TMPDIFF\n"
printf "Generated realizations are in $TMPREAL\n"
res=1
fi
echo "Testing coq realizations"
# First copy current realizations in a tmp directory
cp -r ../lib/coq/ $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_COQ="$TMPREAL/lib/coq" update-coq > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' -x '*~' -x '*.aux' ../lib/coq $TMPREAL/lib/coq`
if test "$TMPDIFF" = "" ; then
printf "Coq realizations OK\n"
else
printf "COQ REALIZATIONS FAILED, please regenerate and prove it\n"
printf "$TMPDIFF\n"
printf "Generated realizations are in $TMPREAL\n"
res=1
fi
......@@ -29,4 +29,4 @@ bin/why3config --detect-provers
make bench
# check that the realizations are ok
examples/regtests.sh --only-realizations
misc/check_realizations.sh
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-2.2.0"
exec = "alt-ergo-1.30"
exec = "alt-ergo-1.01"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
version_ok = "1.30"
version_ok = "2.0.0"
version_old = "1.30"
version_old = "1.01"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
......@@ -347,14 +349,16 @@ version_old = "201310"
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.6.0"
exec = "z3-4.5.0"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.6.0"
version_ok = "4.5.0"
version_ok = "4.4.1"
version_ok = "4.4.0"
version_old = "4.4.1"
version_old = "4.4.0"
driver = "z3_440"
command = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
......@@ -365,14 +369,16 @@ use_at_auto_level = 1
name = "Z3"
alternative = "noBV"
exec = "z3"
exec = "z3-4.6.0"
exec = "z3-4.5.0"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.6.0"
version_ok = "4.5.0"
version_ok = "4.4.1"
version_ok = "4.4.0"
version_old = "4.4.1"
version_old = "4.4.0"
driver = "z3_432"
command = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
......
......@@ -31,16 +31,19 @@ let localdir = $localdir
let compile_time_support = [ @COMPILETIMECOQ@ @COMPILETIMEPVS@ ]
" > $config
if [ "@enable_relocation@" = "no" ]; then
echo "
BINDIR = $bindir
LIBDIR = $libdir
DATADIR = $datadir
OCAMLBEST = @OCAMLBEST@
BIGINTLIB = @BIGINTLIB@
INCLUDE = @BIGINTINCLUDE@ -I @OCAMLINSTALLLIB@/why3
INCLUDEALL = @BIGINTINCLUDE@ @ZIPINCLUDE@ @MENHIRINCLUDE@ -I @OCAMLINSTALLLIB@/why3
" > $makefileconfig
if [ "@enable_relocation@" = "no" ]; then
echo "
BINDIR = $bindir
LIBDIR = $libdir
DATADIR = $datadir
" >> $makefileconfig
fi
......@@ -61,9 +61,9 @@ type prover_autodetection_data =
execs : string list;
version_switch : string;
version_regexp : string;
versions_ok : Str.regexp list;
versions_old : Str.regexp list;
versions_bad : Str.regexp list;
versions_ok : (string * Str.regexp) list;
versions_old : (string * Str.regexp) list;
versions_bad : (string * Str.regexp) list;
(** If none it's a fake prover (very bad version) *)
prover_command : string option;
prover_command_steps : string option;
......@@ -84,7 +84,7 @@ let prover_keys =
let load_prover kind (id,section) =
check_exhaustive section prover_keys;
let reg_map = List.rev_map why3_regexp_of_string in
let reg_map = List.rev_map (fun s -> (s,why3_regexp_of_string s)) in
let prover = { kind = kind;
prover_id = id;
prover_name = get_string section "name";
......@@ -158,7 +158,7 @@ type env =
unknown version (neither good or bad)
| None there is a good version *)
prover_unknown_version :
(int * string * config_prover) option Hstr.t;
(prover_autodetection_data * int * string * config_prover) option Hstr.t;
(* string -> priority * prover *)
prover_shortcuts : (int * prover) Hstr.t;
mutable possible_prover_shortcuts : (filter_prover * string) list;
......@@ -254,15 +254,15 @@ let ask_prover_version env exec_name version_switch =
Hstr2.add env.prover_output (exec_name,version_switch) res;
res
let check_version version schema = Str.string_match schema version 0
let check_version version (_,schema) = Str.string_match schema version 0
let known_version env exec_name =
Hstr.replace env.prover_unknown_version exec_name None
let unknown_version env exec_name prover_id prover_config priority =
let unknown_version env exec_name prover_id prover_config data priority =
if not (Hstr.mem env.prover_unknown_version exec_name)
then Hstr.replace env.prover_unknown_version exec_name
(Some (priority,prover_id,prover_config))
(Some (data,priority,prover_id,prover_config))
let empty_alt s = if s = "" then "alt" else s
......@@ -510,22 +510,29 @@ let detect_exec env data acc exec_name =
if level > 0 then record_prover_for_auto_mode prover level;
add_prover_with_uniq_id prover_config acc
end
else (unknown_version env exec_name data.prover_id prover_config priority;
else (unknown_version env exec_name data.prover_id prover_config data priority;
acc)
let detect_prover env acc data =
List.fold_left (detect_exec env data) acc data.execs
let pp_versions =
Pp.print_list Pp.comma
(Pp.print_pair_delim Pp.nothing Pp.nothing Pp.nothing Pp.string Pp.nothing)
(** add the prover unknown *)
let detect_unknown env detected =
Hstr.fold (fun _ pc acc ->
match pc with
| None -> acc
| Some (priority,prover_id,prover_config) ->
| Some (prover_data,priority,prover_id,prover_config) ->
let prover = prover_config.prover in
Warning.emit "Warning: prover %s version %s is not known to be \
supported.@."
prover.Wc.prover_name prover.prover_version;
Warning.emit "@[Prover %s version %s is not known to be supported.@\n\
Known versions for this prover:@ %a@\n\
Known old versions for this prover:@ %a@]@."
prover.Wc.prover_name prover.prover_version
pp_versions prover_data.versions_ok
pp_versions prover_data.versions_old;
(* Pb: Even if it match the first prover section (normally
highest priority) since it is unknown it has the lower
priority for its id as shortcut. Perhaps we don't want
......
......@@ -929,7 +929,12 @@ let absolute_driver_file main s =
let load_driver main env file extras =
let file = absolute_driver_file main file in
Driver.load_driver_absolute env file extras
try
Driver.load_driver_absolute env file extras