Skip to content

GitLab

why3
why3

Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 7bfbc104 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Merge branch 'master' into itp 

Conflicts:
	examples/dijkstra/why3session.xml
	examples/dijkstra/why3shapes.gz
	src/ide/gmain.ml
	src/session/session.ml
	src/session/session.mli
	src/session/session_scheduler.ml
	src/tools/why3replay.ml
	src/why3session/why3session_copy.ml
	src/why3session/why3session_csv.ml
	src/why3session/why3session_info.ml
	src/why3session/why3session_lib.ml
parents 74299a1a c266cbf3
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 18383 additions and 15943 deletions
examples/WP_revisited/formula/why3session.xml
View file @ 7bfbc104
......@@ -8,8 +8,8 @@
<file name="../formula.why">
<theory name="Formula" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="PropositionalCalculus" sum="8e90228c74fc9a58ce016c323f7a8bff" expanded="true">
<goal name="Test1" expanded="true">
<theory name="PropositionalCalculus" sum="2197343d91936e442b6aeb7d3a3b50db" expanded="true">
<goal name="Test1" expl="" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="46"/></proof>
......
examples/WP_revisited/imp_n/why3session.xml
View file @ 7bfbc104
......@@ -8,61 +8,61 @@
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../imp_n.why" expanded="true">
<theory name="Imp" sum="c5b2f605219b1db882298415fdd56cc4" expanded="true">
<goal name="ident_eq_dec">
<theory name="Imp" sum="4edcb627e6f7cecac2b0d3f266958856" expanded="true">
<goal name="ident_eq_dec" expl="">
<proof prover="6"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
<goal name="check_skip">
<goal name="check_skip" expl="">
<proof prover="6"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="Test13">
<goal name="Test13" expl="">
<proof prover="6"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="Test42">
<goal name="Test42" expl="">
<proof prover="6"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="Test55">
<goal name="Test55" expl="">
<proof prover="6"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="Ass42">
<goal name="Ass42" expl="">
<proof prover="6"><result status="valid" time="0.09" steps="90"/></proof>
</goal>
<goal name="If42">
<goal name="If42" expl="">
<proof prover="5" timelimit="5" memlimit="1000"><result status="valid" time="0.06"/></proof>
<proof prover="6" timelimit="5" memlimit="1000"><result status="valid" time="0.29" steps="489"/></proof>
<proof prover="7"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="progress">
<goal name="progress" expl="">
<proof prover="0" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="steps_non_neg">
<goal name="steps_non_neg" expl="">
<proof prover="0" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="many_steps_seq">
<goal name="many_steps_seq" expl="">
<proof prover="0" edited="imp_n_Imp_many_steps_seq_1.v"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="eval_subst_expr">
<goal name="eval_subst_expr" expl="">
<proof prover="0" edited="imp_n_Imp_eval_subst_expr_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="eval_subst">
<goal name="eval_subst" expl="">
<proof prover="0" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="skip_rule">
<goal name="skip_rule" expl="">
<proof prover="6"><result status="valid" time="0.04" steps="113"/></proof>
</goal>
<goal name="assign_rule">
<goal name="assign_rule" expl="">
<proof prover="0" edited="imp_n_Imp_assign_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="seq_rule">
<goal name="seq_rule" expl="">
<proof prover="0" edited="imp_n_Imp_seq_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="if_rule">
<goal name="if_rule" expl="">
<proof prover="0" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="while_rule">
<goal name="while_rule" expl="">
<proof prover="0" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="consequence_rule">
<goal name="consequence_rule" expl="">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="timeout" time="2.98"/></proof>
</goal>
......
examples/WP_revisited/wp2/why3session.xml
View file @ 7bfbc104
......@@ -7,178 +7,178 @@
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/>
<file name="../wp2.mlw" expanded="true">
<theory name="Imp" sum="128a05171862f85c119bf4cc4ff1493c">
<goal name="eval_subst_term">
<theory name="Imp" sum="4d6ec4c3ea3a39365f84600c953b8179">
<goal name="eval_subst_term" expl="">
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_subst_term_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="eval_term_change_free">
<goal name="eval_term_change_free" expl="">
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_term_change_free_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="eval_subst">
<goal name="eval_subst" expl="">
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_subst_1.v"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="eval_swap">
<goal name="eval_swap" expl="">
<proof prover="2" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="eval_change_free">
<goal name="eval_change_free" expl="">
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_change_free_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="check_skip">
<goal name="check_skip" expl="">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="7" memlimit="0"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="steps_non_neg">
<goal name="steps_non_neg" expl="">
<proof prover="0" edited="wp2_Imp_steps_non_neg_1.v"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="many_steps_seq">
<goal name="many_steps_seq" expl="">
<proof prover="0" edited="wp2_Imp_many_steps_seq_1.v"><result status="valid" time="0.41"/></proof>
</goal>
</theory>
<theory name="TestSemantics" sum="c3f64f8e046da17539cc77734ed8e87c">
<goal name="Test13">
<theory name="TestSemantics" sum="ea9fb18b1935c25df0ce7f228aabf76f">
<goal name="Test13" expl="">
<proof prover="2" memlimit="1000"><result status="valid" time="0.03"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="Test42">
<goal name="Test42" expl="">
<proof prover="2" memlimit="1000"><result status="valid" time="0.04"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="Test0">
<goal name="Test0" expl="">
<proof prover="2" memlimit="1000"><result status="valid" time="0.04"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="Test55">
<goal name="Test55" expl="">
<proof prover="0" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_Test55_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="Ass42">
<goal name="Ass42" expl="">
<proof prover="2" memlimit="1000"><result status="valid" time="0.04"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.06" steps="100"/></proof>
</goal>
<goal name="If42">
<goal name="If42" expl="">
<proof prover="0" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_If42_1.v"><result status="valid" time="1.00"/></proof>
</goal>
</theory>
<theory name="HoareLogic" sum="82e50c9c6ac0f07e1bde1792daeea9d0">
<goal name="consequence_rule">
<theory name="HoareLogic" sum="ac7395abbc54f2eaf2a4731bbadf3a7c">
<goal name="consequence_rule" expl="">
<proof prover="2" memlimit="1000"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="skip_rule">
<goal name="skip_rule" expl="">
<proof prover="0" edited="wp2_HoareLogic_skip_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="assign_rule">
<goal name="assign_rule" expl="">
<proof prover="0" edited="wp2_HoareLogic_assign_rule_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="seq_rule">
<goal name="seq_rule" expl="">
<proof prover="5" timelimit="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="if_rule">
<goal name="if_rule" expl="">
<proof prover="0" edited="wp2_HoareLogic_if_rule_1.v"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="assert_rule">
<goal name="assert_rule" expl="">
<proof prover="0" edited="wp2_HoareLogic_assert_rule_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="assert_rule_ext">
<goal name="assert_rule_ext" expl="">
<proof prover="0" edited="wp2_HoareLogic_assert_rule_ext_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="while_rule">
<goal name="while_rule" expl="">
<proof prover="0" edited="wp2_HoareLogic_while_rule_1.v"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="while_rule_ext">
<goal name="while_rule_ext" expl="">
<proof prover="0" edited="wp2_HoareLogic_while_rule_ext_1.v"><result status="valid" time="0.54"/></proof>
</goal>
</theory>
<theory name="WP" sum="60d483dfb3680562a74d6cbbecffcb0d">
<goal name="assigns_refl">
<theory name="WP" sum="ac7e95b3f1136de0ba1a9054f4091dbf">
<goal name="assigns_refl" expl="">
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.02" steps="3"/></proof>
</goal>
<goal name="assigns_trans">
<goal name="assigns_trans" expl="">
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="assigns_union_left">
<goal name="assigns_union_left" expl="">
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="assigns_union_right">
<goal name="assigns_union_right" expl="">
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter compute_writes" expl="VC for compute_writes">
<transf name="split_goal_wp">
<goal name="WP_parameter compute_writes.1" expl="1. postcondition">
<goal name="WP_parameter compute_writes.1" expl="postcondition">
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.06" steps="94"/></proof>
</goal>
<goal name="WP_parameter compute_writes.2" expl="2. postcondition">
<goal name="WP_parameter compute_writes.2" expl="postcondition">
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_1.v"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="WP_parameter compute_writes.3" expl="3. variant decrease">
<goal name="WP_parameter compute_writes.3" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="42"/></proof>
</goal>
<goal name="WP_parameter compute_writes.4" expl="4. variant decrease">
<goal name="WP_parameter compute_writes.4" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="43"/></proof>
</goal>
<goal name="WP_parameter compute_writes.5" expl="5. postcondition">
<goal name="WP_parameter compute_writes.5" expl="postcondition">
<proof prover="5" timelimit="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter compute_writes.6" expl="6. variant decrease">
<goal name="WP_parameter compute_writes.6" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.03" steps="47"/></proof>
</goal>
<goal name="WP_parameter compute_writes.7" expl="7. variant decrease">
<goal name="WP_parameter compute_writes.7" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="48"/></proof>
</goal>
<goal name="WP_parameter compute_writes.8" expl="8. postcondition">
<goal name="WP_parameter compute_writes.8" expl="postcondition">
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_3.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="WP_parameter compute_writes.9" expl="9. variant decrease">
<goal name="WP_parameter compute_writes.9" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="47"/></proof>
</goal>
<goal name="WP_parameter compute_writes.10" expl="10. postcondition">
<goal name="WP_parameter compute_writes.10" expl="postcondition">
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_4.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="WP_parameter compute_writes.11" expl="11. postcondition">
<goal name="WP_parameter compute_writes.11" expl="postcondition">
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_2.v"><result status="valid" time="0.34"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter wp" expl="VC for wp">
<transf name="split_goal_wp">
<goal name="WP_parameter wp.1" expl="1. postcondition">
<goal name="WP_parameter wp.1" expl="postcondition">
<proof prover="2" timelimit="3"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter wp.2" expl="2. variant decrease">
<goal name="WP_parameter wp.2" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.03" steps="42"/></proof>
</goal>
<goal name="WP_parameter wp.3" expl="3. variant decrease">
<goal name="WP_parameter wp.3" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.03" steps="44"/></proof>
</goal>
<goal name="WP_parameter wp.4" expl="4. postcondition">
<goal name="WP_parameter wp.4" expl="postcondition">
<proof prover="2" timelimit="3"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.12"/></proof>
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter wp.5" expl="5. postcondition">
<goal name="WP_parameter wp.5" expl="postcondition">
<proof prover="2" timelimit="3"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.11"/></proof>
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter wp.6" expl="6. variant decrease">
<goal name="WP_parameter wp.6" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.03" steps="47"/></proof>
</goal>
<goal name="WP_parameter wp.7" expl="7. variant decrease">
<goal name="WP_parameter wp.7" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="49"/></proof>
</goal>
<goal name="WP_parameter wp.8" expl="8. postcondition">
<goal name="WP_parameter wp.8" expl="postcondition">
<proof prover="0" edited="wp2_WP_WP_WP_parameter_wp_1.v"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="WP_parameter wp.9" expl="9. postcondition">
<goal name="WP_parameter wp.9" expl="postcondition">
<proof prover="2" timelimit="3"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.11"/></proof>
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter wp.10" expl="10. variant decrease">
<goal name="WP_parameter wp.10" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="47"/></proof>
</goal>
<goal name="WP_parameter wp.11" expl="11. postcondition">
<goal name="WP_parameter wp.11" expl="postcondition">
<proof prover="0" timelimit="5" edited="wp2_WP_WP_WP_parameter_wp_2.v"><result status="valid" time="0.87"/></proof>
</goal>
</transf>
......
examples/add_list/why3session.xml
View file @ 7bfbc104
......@@ -8,7 +8,7 @@
<file name="../add_list.mlw" expanded="true">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="AddListRec" sum="f062b1e05a91602624b37c4b34762555" expanded="true">
<theory name="AddListRec" sum="ddf9071b1a9688fe9218a8b95f77634f" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -19,7 +19,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="AddListImp" sum="7ac8c0163d88693d0911255c23bfb93d" expanded="true">
<theory name="AddListImp" sum="b8d9e3c0e71fb300ad846cc5060783ef" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
......
examples/algo63/why3session.xml
View file @ 7bfbc104
This diff is collapsed.
examples/algo64/why3session.xml
View file @ 7bfbc104
......@@ -4,59 +4,59 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../algo64.mlw" expanded="true">
<theory name="Algo64" sum="8ab02ef07be464ccc7c31dda9dd33adb" expanded="true">
<theory name="Algo64" sum="51d805a22bc2e9af151efc73086f3b23" expanded="true">
<goal name="WP_parameter quicksort" expl="VC for quicksort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter quicksort.1" expl="1. precondition">
<goal name="WP_parameter quicksort.1" expl="precondition">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter quicksort.2" expl="2. variant decrease">
<goal name="WP_parameter quicksort.2" expl="variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter quicksort.3" expl="3. precondition">
<goal name="WP_parameter quicksort.3" expl="precondition">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter quicksort.4" expl="4. assertion">
<goal name="WP_parameter quicksort.4" expl="assertion">
<proof prover="1"><result status="valid" time="0.14" steps="131"/></proof>
</goal>
<goal name="WP_parameter quicksort.5" expl="5. variant decrease">
<goal name="WP_parameter quicksort.5" expl="variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter quicksort.6" expl="6. precondition">
<goal name="WP_parameter quicksort.6" expl="precondition">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter quicksort.7" expl="7. assertion">
<goal name="WP_parameter quicksort.7" expl="assertion">
<proof prover="1"><result status="valid" time="1.43" steps="657"/></proof>
</goal>
<goal name="WP_parameter quicksort.8" expl="8. postcondition">
<goal name="WP_parameter quicksort.8" expl="postcondition">
<proof prover="1"><result status="valid" time="0.19" steps="315"/></proof>
</goal>
<goal name="WP_parameter quicksort.9" expl="9. postcondition">
<goal name="WP_parameter quicksort.9" expl="postcondition">
<proof prover="1"><result status="valid" time="0.16" steps="95"/></proof>
</goal>
<goal name="WP_parameter quicksort.10" expl="10. postcondition">
<goal name="WP_parameter quicksort.10" expl="postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter quicksort.11" expl="11. postcondition">
<goal name="WP_parameter quicksort.11" expl="postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter qs" expl="VC for qs">
<transf name="split_goal_wp">