Commit 227a8587 authored by MARCHE Claude's avatar MARCHE Claude

Almost ready for release

parent 28106e2c
* marks an incompatible change
o [Sessions] a small change in the format. Why3 is still able to
read session files in the old format.
o completed support for the "Out Of Memory" prover result
o [Why3ml] new construct "abstract e { q }"
o [Coq output] quotes in identifiers remain quotes in Coq
......@@ -8,7 +10,7 @@
o [why3replayer] option -obsolete-only
o workaround for a bug about modulo operator in Alt-Ergo 0.94
o fixed a consistency issue with set.Fset theory
o co-inductive predicates (experimental)
o co-inductive predicates
o new option -e for "why3session latex" allows to specify when to
split tables in parts
......
......@@ -132,7 +132,6 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* detect editors
*** check if coqide and also emacs/proof-general is installed
* IDE
** todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
......@@ -157,6 +156,10 @@ New features:
o co-inductive predicates
o new option -e for "why3session latex" allows to specify when to
split tables in parts
o [Sessions] a small change in the format. This hopefully improves
the association of old goals and new goals when the input is
modified. For compatibility, Why3 is still able to read session
files in the old format.
Bug fix:
o completed support for the "Out Of Memory" prover result
......@@ -203,7 +206,7 @@ Bug fix:
** DONE option pour ne rejouer que si obsolete
* Documentation
- document co-inductive predicates ?
- DELAYED document co-inductive predicates
- DONE (CLAUDE) revoir documentation du smoke detector
==================== Roadmap for release 0.72 ========================
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="programs/hash_tables/why3session.xml" shape_version="2">
name="examples/programs/hash_tables/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95-dev"/>
<prover
id="2"
name="CVC3"
version="2.2"/>
<prover
id="2"
id="3"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
id="4"
name="Coq"
version="8.3pl4"/>
<prover
id="4"
id="5"
name="Z3"
version="2.19"/>
<prover
id="5"
id="6"
name="Z3"
version="3.2"/>
<file
name="../hash_tables.mlw"
verified="true"
expanded="false">
expanded="true">
<theory
name="WP HashTable"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="10" loccnumb="7" loccnume="16"
verified="true"
expanded="false">
</theory>
<theory
name="WP HashTableImpl"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="41" loccnumb="7" loccnume="20"
verified="true"
expanded="false">
expanded="true">
<goal
name="mem_occurs_first"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="68" loccnumb="8" loccnume="24"
sum="8877339accd60b88826efe1680824c5c"
proved="true"
expanded="false"
shape="amemaTuple2V0V1V2Iaoccurs_firstV0V1V2F">
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
edited="hash_tables_WP_HashTableImpl_mem_occurs_first_2.v"
......@@ -63,32 +67,48 @@
</goal>
<goal
name="cons_occurs_first"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="72" loccnumb="8" loccnume="25"
sum="bfb8b9d44f3164146df0c2c4eba8e82f"
proved="true"
expanded="false"
shape="aoccurs_firstV0V1aConsaTuple2V3V4V2Iainfix =V3V0NFIaoccurs_firstV0V1V2F">
<proof
prover="4"
timelimit="20"
memlimit="0"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="1"
timelimit="20"
memlimit="0"
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="20"
memlimit="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -96,16 +116,56 @@
</goal>
<goal
name="idx_bounds"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="86" loccnumb="8" loccnume="18"
sum="f0226fa4275508a5bae7ec9efa6be522"
proved="true"
expanded="false"
shape="ainfix &lt;aidxV0V1alengthadataV0Aainfix &lt;=c0aidxV0V1FIavalidV0F">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
timelimit="15"
memlimit="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
......@@ -113,7 +173,7 @@
</goal>
<goal
name="WP_parameter create"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="89" loccnumb="6" loccnume="12"
expl="parameter create"
sum="67d699e15ed7eef115e6366f61d9befa"
......@@ -123,9 +183,17 @@
<label
name="expl:parameter create"/>
<proof
prover="4"
timelimit="10"
memlimit="0"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
......@@ -133,7 +201,7 @@
</goal>
<goal
name="WP_parameter clear"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="95" loccnumb="6" loccnume="11"
expl="parameter clear"
sum="b8293fb0af655ea500be6393fa0ee3ea"
......@@ -148,7 +216,7 @@
expanded="false">
<goal
name="WP_parameter clear.1"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="95" loccnumb="6" loccnume="11"
expl="precondition"
sum="42c9d0f28eb79dff81c195e1079a3b26"
......@@ -157,18 +225,58 @@
shape="ainfix &lt;=ainfix +c0V0V0Aainfix &lt;=c0c0Iavalidamk tV2amk arrayV0V1FFF">
<label
name="expl:parameter clear"/>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="10"
memlimit="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter clear.2"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="95" loccnumb="6" loccnume="11"
expl="normal postcondition"
sum="b087f3b923ce9751f663295c85a7188e"
......@@ -183,7 +291,7 @@
expanded="false">
<goal
name="WP_parameter clear.2.1"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="95" loccnumb="6" loccnume="11"
expl="normal postcondition"
sum="f69455c4bc9132de4fa8a638f80b2f66"
......@@ -198,7 +306,7 @@
expanded="false">
<goal
name="WP_parameter clear.2.1.1"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="95" loccnumb="6" loccnume="11"
expl="parameter clear"
sum="34039b3d034762636d45b6fbd30527a0"
......@@ -207,10 +315,50 @@
shape="ainfix &gt;alengthadataamk tV4amk arrayV0V3c0Iainfix =V4aconstaNoneFIainfix =agetV3V5aNilIainfix &lt;V5ainfix +c0V0Aainfix =c0V5Oainfix &lt;c0V5FAainfix =agetV3V6agetV1V6Iainfix &lt;V6V0Aainfix =ainfix +c0V0V6Oainfix &lt;ainfix +c0V0V6Oainfix &lt;V6c0Aainfix =c0V6Oainfix &lt;c0V6FFIainfix =ainfix +c0V0V0Oainfix &lt;ainfix +c0V0V0Aainfix =c0c0Oainfix &lt;c0c0Iainfix =V9aidxamk tV2amk arrayV0V1V7IamemaTuple2V7V8amixfix []adataamk tV2amk arrayV0V1V9Iainfix &lt;V9alengthadataamk tV2amk arrayV0V1Aainfix &lt;=c0V9FFAaoccurs_firstV10V11amixfix []adataamk tV2amk arrayV0V1aidxamk tV2amk arrayV0V1V10qainfix =agetamk tV2amk arrayV0V1V10aSomeV11FAainfix &gt;alengthadataamk tV2amk arrayV0V1c0FFF">
<label
name="expl:parameter clear"/>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
timelimit="10"
memlimit="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -218,7 +366,7 @@
</goal>
<goal
name="WP_parameter clear.2.1.2"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="95" loccnumb="6" loccnume="11"
expl="parameter clear"
sum="a2c3cf6d9093166bb3242a7760d2278b"
......@@ -228,17 +376,57 @@
<label
name="expl:parameter clear"/>
<proof
prover="1"
timelimit="10"
memlimit="0"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.51"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.52"/>
</proof>
</goal>
<goal
name="WP_parameter clear.2.1.3"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="95" loccnumb="6" loccnume="11"
expl="parameter clear"
sum="ff5fe42741dac92977c300c17c5570c3"
......@@ -247,18 +435,58 @@
shape="ainfix =agetamk tV4amk arrayV0V3V5aSomeV6Iaoccurs_firstV5V6amixfix []adataamk tV4amk arrayV0V3aidxamk tV4amk arrayV0V3V5FIainfix =V4aconstaNoneFIainfix =agetV3V7aNilIainfix &lt;V7ainfix +c0V0Aainfix =c0V7Oainfix &lt;c0V7FAainfix =agetV3V8agetV1V8Iainfix &lt;V8V0Aainfix =ainfix +c0V0V8Oainfix &lt;ainfix +c0V0V8Oainfix &lt;V8c0Aainfix =c0V8Oainfix &lt;c0V8FFIainfix =ainfix +c0V0V0Oainfix &lt;ainfix +c0V0V0Aainfix =c0c0Oainfix &lt;c0c0Iainfix =V11aidxamk tV2amk arrayV0V1V9IamemaTuple2V9V10amixfix []adataamk tV2amk arrayV0V1V11Iainfix &lt;V11alengthadataamk tV2amk arrayV0V1Aainfix &lt;=c0V11FFAaoccurs_firstV12V13amixfix []adataamk tV2amk arrayV0V1aidxamk tV2amk arrayV0V1V12qainfix =agetamk tV2amk arrayV0V1V12aSomeV13FAainfix &gt;alengthadataamk tV2amk arrayV0V1c0FFF">
<label
name="expl:parameter clear"/>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
</proof>
<proof
prover="0"
timelimit="10"
memlimit="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.70"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.69"/>
<result status="valid" time="0.10"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.65"/>
</proof>
</goal>
<goal
name="WP_parameter clear.2.1.4"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="95" loccnumb="6" loccnume="11"
expl="parameter clear"
sum="93e243e2597e4bce81ee2f672cb9f19d"
......@@ -267,18 +495,58 @@
shape="ainfix =V7aidxamk tV4amk arrayV0V3V5IamemaTuple2V5V6amixfix []adataamk tV4amk arrayV0V3V7Iainfix &lt;V7alengthadataamk tV4amk arrayV0V3Aainfix &lt;=c0V7FFIainfix =V4aconstaNoneFIainfix =agetV3V8aNilIainfix &lt;V8ainfix +c0V0Aainfix =c0V8Oainfix &lt;c0V8FAainfix =agetV3V9agetV1V9Iainfix &lt;V9V0Aainfix =ainfix +c0V0V9Oainfix &lt;ainfix +c0V0V9Oainfix &lt;V9c0Aainfix =c0V9Oainfix &lt;c0V9FFIainfix =ainfix +c0V0V0Oainfix &lt;ainfix +c0V0V0Aainfix =c0c0Oainfix &lt;c0c0Iainfix =V12aidxamk tV2amk arrayV0V1V10IamemaTuple2V10V11amixfix []adataamk tV2amk arrayV0V1V12Iainfix &lt;V12alengthadataamk tV2amk arrayV0V1Aainfix &lt;=c0V12FFAaoccurs_firstV13V14amixfix []adataamk tV2amk arrayV0V1aidxamk tV2amk arrayV0V1V13qainfix =agetamk tV2amk arrayV0V1V13aSomeV14FAainfix &gt;alengthadataamk tV2amk arrayV0V1c0FFF">
<label
name="expl:parameter clear"/>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="0"
timelimit="10"
memlimit="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.78"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.75"/>
</proof>
</goal>
<goal
name="WP_parameter clear.2.1.5"
locfile="programs/hash_tables/../hash_tables.mlw"
locfile="examples/programs/hash_tables/../hash_tables.mlw"
loclnum="95" loccnumb="6" loccnume="11"
expl="parameter clear"
sum="41b2cd35b813d67000310faae971e1a6"
......@@ -287,13 +555,53 @@
shape="ainfix =agetV4V5aNoneFIainfix =V4aconstaNoneFIainfix =agetV3V6aNilIainfix &lt;V6ainfix +c0V0Aainfix =c0V6Oainfix &lt;c0V6FAainfix =agetV3V7agetV1V7Iainfix &lt;V7V0Aainfix =ainfix +c0V0V7Oainfix &lt;ainfix +c0V0V7Oainfix &lt;V7c0Aainfix =c0V7Oainfix &lt;c0V7FFIainfix =ainfix +c0V0V0Oainfix &lt;ainfix +c0V0V0Aainfix =c0c0Oainfix &lt;c0c0Iainfix =V10aidxamk tV2amk arrayV0V1V8IamemaTuple2V8V9amixfix []adataamk tV2amk arrayV0V1V10Iainfix &lt;V10alengthadataamk tV2amk arrayV0V1Aainfix &lt;=c0V10FFAaoccurs_firstV11V12amixfix []adataamk tV2amk arrayV0V1aidxamk tV2amk arrayV0V1V11qainfix =agetamk tV2amk arrayV0V1V11aSomeV12FAainfix &gt;alengthadataamk tV2amk arrayV0V1c0FFF">
<label
name="expl:parameter clear"/>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
timelimit="10"
memlimit="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"