Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 082d207d authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Merge branch 'master' into mp

parents ae1207f9 96ba61b6
: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
--------------------------------
......
......@@ -1739,7 +1739,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
@if test "@enable_coq_tactic@" = "yes"; then \
echo ; \
echo "=== Checking the Coq tactic ==="; \
$(MAKE) test-coq-tactic.@OCAMLBEST@; fi
$(MAKE) test-coq-tactic; fi
###############
# test targets
......
......@@ -9,7 +9,7 @@
suffix=$1
# TODO: remove the hack about int.why once it has become builtin
# TODO: remove the hack about int.mlw once it has become builtin
goods () {
pgm="bin/why3prove$suffix"
ERROR=
......@@ -17,7 +17,7 @@ goods () {
for f in $1/*.[wm][hl][yw] ; do
printf " $f... "
opts="$2"
if test $f = stdlib/int.why; then opts="$2 --type-only"; fi
if test $f = stdlib/int.mlw; then opts="$2 --type-only"; fi
# running Why
if ! $pgm $opts $f > /dev/null 2> bench_error; then
echo "FAILED!"
......
......@@ -253,6 +253,21 @@ module mach.int.State63
syntax val random_int63 "SHOULD_NOT_BE_HERE"
end
module set.Fset
syntax val mem "SHOULD_NOT_BE_HERE"
syntax val (==) "SHOULD_NOT_BE_HERE"
syntax val subset "SHOULD_NOT_BE_HERE"
syntax val is_empty "SHOULD_NOT_BE_HERE"
syntax val empty "SHOULD_NOT_BE_HERE"
syntax val add "SHOULD_NOT_BE_HERE"
syntax val remove "SHOULD_NOT_BE_HERE"
syntax val union "SHOULD_NOT_BE_HERE"
syntax val inter "SHOULD_NOT_BE_HERE"
syntax val diff "SHOULD_NOT_BE_HERE"
syntax val choose "SHOULD_NOT_BE_HERE"
syntax val cardinal "SHOULD_NOT_BE_HERE"
end
module mach.peano.Peano
syntax type t "int"
syntax val to_int "Z.of_int %1"
......
......@@ -433,16 +433,16 @@ module AVL
ensures { let hl = l.hgt in let hr = r.hgt in
let he = 1 + if hl < hr then hr else hl in let hres = result.hgt in
0 <= he - hres <= 1 }
variant { l.hgt + r.hgt }
variant { if l.hgt > r.hgt then l.hgt - r.hgt else r.hgt - l.hgt }
= match view l with
| AEmpty -> cons d r
| ANode ll ld lr lh _ -> match view r with
| AEmpty -> snoc l d
| ANode rl rd rr rh _ ->
let df = I.sub lh rh (I.neg rh) lh in
if I.ge df balancing
if I.gt df balancing
then balance ll ld (join lr d r)
else if I.le df (I.neg balancing)
else if I.lt df (I.neg balancing)
then balance (join l d rl) rd rr
else node l d r
end
......
This diff is collapsed.
theory T
goal g : forall x:int. x = (x at L)
end
......@@ -76,6 +76,43 @@ module BinarySearchAnyMidPoint
end
(* The following version of binary search is faster in practice, by being
friendlier with the branch predictor of most processors. It also happens
to be stable, since it always return the highest index. *)
module BinarySearchBranchless
use import int.Int
use import int.ComputerDivision
use import ref.Ref
use import array.Array
exception Not_found (* raised to signal a search failure *)
let binary_search (a : array int) (v : int) : int
requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
ensures { 0 <= result < length a /\ a[result] = v }
ensures { forall i : int. result < i < length a -> a[i] <> v }
raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
=
let l = ref 0 in
let s = ref (length a) in
if !s = 0 then raise Not_found;
while !s > 1 do
invariant { 0 <= !l /\ !l + !s <= length a /\ !s >= 1 }
invariant {
forall i : int. 0 <= i < length a -> a[i] = v -> a[!l] <= v /\ i < !l + !s }
variant { !s }
let h = div !s 2 in
let m = !l + h in
l := if a[m] > v then !l else m;
s := !s - h;
done;
if a[!l] = v then !l
else raise Not_found
end
(* binary search using 32-bit integers *)
module BinarySearchInt32
......@@ -85,8 +122,6 @@ module BinarySearchInt32
use import ref.Ref
use import mach.array.Array32
(* the code and its specification *)
exception Not_found (* raised to signal a search failure *)
let binary_search (a : array int32) (v : int32) : int32
......
......@@ -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="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_search.mlw" proved="true">
<theory name="BinarySearch" proved="true" sum="a87eac5cc232a78b8d8da4a5e55ee897">
......@@ -14,6 +15,11 @@
<proof prover="3"><result status="valid" time="0.01" steps="63"/></proof>
</goal>
</theory>
<theory name="BinarySearchBranchless" proved="true" sum="3b2dad84c0bdc39e32b7664b11a669ff">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="147"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" proved="true" sum="189de117608870d3dac4a21f7234eef5">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="3"><result status="valid" time="8.18" steps="11481"/></proof>
......
......@@ -19,33 +19,43 @@
<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="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" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Goals" sum="59dc19f9f217c19fb5b57fc86bd98c29" expanded="true">
<goal name="G1">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<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="valid" time="1.08"/></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="1.90"/></proof>
<proof prover="9"><result status="valid" time="0.52"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="timeout" time="1.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="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="1.01"/></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="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">
<proof prover="0"><result status="timeout" time="1.01"/></proof>
<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>
......@@ -53,34 +63,44 @@
<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.79"/></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="11"><result status="timeout" time="1.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="2.07"/></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.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">
<proof prover="0"><result status="timeout" time="1.01"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<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="timeout" time="1.00"/></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="1.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.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.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,41 +2,44 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="CVC4" version="1.2" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="2" name="Zenon" version="0.8.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="4" name="Eprover" version="1.6" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="2.19" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC3" version="2.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="8" name="Eprover" version="1.4" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="9" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="10" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="11" name="Simplify" version="1.5.4" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="12" name="Yices" version="1.0.38" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="13" name="Zenon" version="0.7.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="14" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="15" name="Metis" version="2.3" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="16" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="17" name="Alt-Ergo" version="0.95.2" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="18" name="PVS" version="6.0" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="19" name="veriT" version="201310" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="20" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="21" name="CVC4" version="1.3" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="22" name="Vampire" version="0.6" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="23" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="24" name="veriT" version="201410" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<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"/>
<prover id="4" name="Eprover" version="1.6" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="5" name="Z3" version="2.19" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="CVC3" version="2.2" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="8" name="Eprover" version="1.4" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="9" name="Spass" version="3.7" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="10" name="Z3" version="4.3.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="11" name="Simplify" version="1.5.4" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="12" name="Yices" version="1.0.38" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="13" name="Zenon" version="0.7.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="14" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="15" name="Metis" version="2.3" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="16" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="17" name="Alt-Ergo" version="0.95.2" timelimit="60" steplimit="1" memlimit="1000"/>
<prover id="18" name="PVS" version="6.0" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="19" name="veriT" version="201310" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="20" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="21" name="CVC4" version="1.3" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="22" name="Vampire" version="0.6" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="23" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="24" name="veriT" version="201410" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="27" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="28" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="28" name="Z3" version="4.4.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="29" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="30" name="Isabelle" version="2016-1" timelimit="100" steplimit="0" memlimit="1000"/>
<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="0" memlimit="4000"/>
<file name="../genealogy.why" proved="true">
<theory name="Genealogy" proved="true" sum="b8808df4e10c57dcf1f51dac29bd957e">
<goal name="Child_is_son_or_daughter" proved="true">
<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" 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>
......@@ -62,11 +65,13 @@
<proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="9.99"/></proof>
<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.26"/></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" proved="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>
......@@ -93,10 +98,12 @@
<proof prover="27"><result status="valid" time="0.00"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof>
<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="10.11"/></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" proved="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>
......@@ -121,10 +128,12 @@
<proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<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="10.02"/></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" proved="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>
......@@ -150,10 +159,12 @@
<proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<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="10.24"/></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" proved="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" proved="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" proved="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>
......
......@@ -103,6 +103,15 @@ target_name = "Coq"
target_version = "$COQVER"
version = "8.6"
[uninstalled_prover coq861]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.6.1"
EOF
fi
......@@ -128,9 +137,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 +155,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,7 +65,6 @@ run_dir () {
shapes="$shapes $1/*/why3shapes.*"
}
if test "$ONLY_REALIZATION" = "" ; then
echo "=== Programs already ported === MUST REPLAY AND ALL GOALS PROVED ==="
echo ""
run_dir .
......@@ -163,11 +115,5 @@ 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