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 4868b088 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Fixed non replayed proof for double_wp/compiler

parent c3f99bd1
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<prover id="0" name="Z3" version="4.4.0" timelimit="20" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="7" name="Coq" version="8.4pl6" timelimit="5" memlimit="1000"/>
<file name="../compiler.mlw" expanded="true">
......@@ -248,7 +248,7 @@
</transf>
</goal>
</theory>
<theory name="Compile_bexpr" sum="188f58e34240879911b84d7829c28ad6">
<theory name="Compile_bexpr" sum="e08e81e0609cedfb34c0e36bb92ecb4a">
<goal name="WP_parameter compile_bexpr" expl="VC for compile_bexpr">
<transf name="split_goal_wp">
<goal name="WP_parameter compile_bexpr.1" expl="1. precondition">
......@@ -462,7 +462,7 @@
<proof prover="2"><result status="valid" time="0.38" steps="202"/></proof>
</goal>
<goal name="WP_parameter compile_bexpr.34.1.1.6" expl="6. VC for compile_bexpr">
<proof prover="2"><result status="valid" time="0.28" steps="172"/></proof>
<proof prover="2"><result status="valid" time="0.50" steps="172"/></proof>
</goal>
</transf>
</goal>
......@@ -683,1020 +683,1066 @@
</transf>
</goal>
<goal name="WP_parameter compile_bexpr_natural" expl="VC for compile_bexpr_natural">
<metas>
<ts_pos name="real" arity="0" id="2"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_library name="BuiltIn"/>
<ip_qualid name="real"/>
</ts_pos>
<ts_pos name="pred" arity="1" id="8"
ip_theory="HighOrd">
<ip_library name="why3"/>
<ip_library name="HighOrd"/>
<ip_qualid name="pred"/>
</ts_pos>
<ts_pos name="unit" arity="0" id="21"
ip_theory="Unit">
<ip_library name="why3"/>
<ip_library name="Unit"/>
<ip_qualid name="unit"/>
</ts_pos>
<ts_pos name="&apos;mark" arity="0" id="68"
ip_theory="Mark">
<ip_library name="why3"/>
<ip_library name="Mark"/>
<ip_qualid name="&apos;mark"/>
</ts_pos>
<ts_pos name="tuple2" arity="2" id="1444"
ip_theory="Tuple2">
<ip_library name="why3"/>
<ip_library name="Tuple2"/>
<ip_qualid name="tuple2"/>
</ts_pos>
<ts_pos name="state" arity="0" id="4852"
ip_theory="State">
<ip_library name="state"/>
<ip_qualid name="state"/>
</ts_pos>
<ts_pos name="com" arity="0" id="4866"
ip_theory="Imp">
<ip_library name="imp"/>
<ip_qualid name="com"/>
</ts_pos>
<ts_pos name="pos" arity="0" id="5130"
ip_theory="Vm">
<ip_library name="vm"/>
<ip_qualid name="pos"/>
</ts_pos>
<ts_pos name="stack" arity="0" id="5131"
ip_theory="Vm">
<ip_library name="vm"/>
<ip_qualid name="stack"/>
</ts_pos>
<ts_pos name="code" arity="0" id="5148"
ip_theory="Vm">
<ip_library name="vm"/>
<ip_qualid name="code"/>
</ts_pos>
<ts_pos name="pred" arity="0" id="5536"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="pred"/>
</ts_pos>
<ts_pos name="rel" arity="0" id="5537"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="rel"/>
</ts_pos>
<ts_pos name="post" arity="1" id="5539"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="post"/>
</ts_pos>
<ts_pos name="wp_trans" arity="1" id="5546"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="wp_trans"/>
</ts_pos>
<ts_pos name="wp" arity="1" id="5547"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="wp"/>
</ts_pos>
<ts_pos name="binop" arity="0" id="6240"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="binop"/>
</ts_pos>
<ts_pos name="cond" arity="0" id="6620"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="cond"/>
</ts_pos>
<ls_pos name="infix =" id="10"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_library name="BuiltIn"/>
<ip_qualid name="infix ="/>
</ls_pos>
<ls_pos name="infix @" id="15"
ip_theory="HighOrd">
<ip_library name="why3"/>
<ip_library name="HighOrd"/>
<ip_qualid name="infix @"/>
</ls_pos>
<ls_pos name="zero" id="728"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="one" id="729"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="one"/>
</ls_pos>
<ls_pos name="infix &lt;" id="730"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &lt;"/>
</ls_pos>
<ls_pos name="infix &gt;" id="733"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &gt;"/>
</ls_pos>
<ls_pos name="infix +" id="1899"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix +"/>
</ls_pos>
<ls_pos name="prefix -" id="1900"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="prefix -"/>
</ls_pos>
<ls_pos name="infix *" id="1901"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix *"/>
</ls_pos>
<ls_pos name="infix &gt;=" id="1969"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &gt;="/>
</ls_pos>
<ls_pos name="abs" id="2014"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="abs"/>
</ls_pos>
<ls_pos name="div" id="2139"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="div"/>
</ls_pos>
<ls_pos name="mod" id="2142"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="mod"/>
</ls_pos>
<ls_pos name="mem" id="2778"
ip_theory="Mem">
<ip_library name="list"/>
<ip_qualid name="mem"/>
</ls_pos>
<ls_pos name="orb" id="3864"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="orb"/>
</ls_pos>
<ls_pos name="xorb" id="3878"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="xorb"/>
</ls_pos>
<ls_pos name="implb" id="3887"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="implb"/>
</ls_pos>
<ls_pos name="get" id="4812"
ip_theory="State">
<ip_library name="state"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="4813"
ip_theory="State">
<ip_library name="state"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="ceval" id="4965"
ip_theory="Imp">
<ip_library name="imp"/>
<ip_qualid name="ceval"/>
</ls_pos>
<ls_pos name="ihalt" id="5230"
ip_theory="Vm">
<ip_library name="vm"/>
<ip_qualid name="ihalt"/>
</ls_pos>
<ls_pos name="vm_terminates" id="5481"
ip_theory="Vm">
<ip_library name="vm"/>
<ip_qualid name="vm_terminates"/>
</ls_pos>
<ls_pos name="fst" id="5501"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="fst"/>
</ls_pos>
<ls_pos name="snd" id="5520"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="snd"/>
</ls_pos>
<ls_pos name="wp_correctness" id="5599"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="wp_correctness"/>
</ls_pos>
<ls_pos name="seq_wp" id="5625"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="seq_wp"/>
</ls_pos>
<ls_pos name="fork_wp" id="5714"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="fork_wp"/>
</ls_pos>
<ls_pos name="towp_wp" id="5774"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="towp_wp"/>
</ls_pos>
<ls_pos name="acc" id="5885"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="acc"/>
</ls_pos>
<ls_pos name="forget_old" id="5935"
ip_theory="Compiler_logic">
<ip_library name="logic"/>
<ip_qualid name="forget_old"/>
</ls_pos>
<ls_pos name="ifun_post" id="5985"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="ifun_post"/>
</ls_pos>
<ls_pos name="iconst_post" id="6038"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="iconst_post"/>
</ls_pos>
<ls_pos name="iconst_fun" id="6072"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="iconst_fun"/>
</ls_pos>
<ls_pos name="ivar_post" id="6139"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="ivar_post"/>
</ls_pos>
<ls_pos name="ivar_fun" id="6173"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="ivar_fun"/>
</ls_pos>
<ls_pos name="ibinop_pre" id="6241"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="ibinop_pre"/>
</ls_pos>
<ls_pos name="ibinop_post" id="6274"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="ibinop_post"/>
</ls_pos>
<ls_pos name="ibinop_fun" id="6316"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="ibinop_fun"/>
</ls_pos>
<ls_pos name="plus" id="6415"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="plus"/>
</ls_pos>
<ls_pos name="sub" id="6428"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="sub"/>
</ls_pos>
<ls_pos name="mul" id="6441"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="mul"/>
</ls_pos>
<ls_pos name="inil_post" id="6487"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="inil_post"/>
</ls_pos>
<ls_pos name="ibranch_post" id="6519"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="ibranch_post"/>
</ls_pos>
<ls_pos name="ibranch_fun" id="6553"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="ibranch_fun"/>
</ls_pos>
<ls_pos name="icjump_post" id="6621"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="icjump_post"/>
</ls_pos>
<ls_pos name="icjump_fun" id="6668"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="icjump_fun"/>
</ls_pos>
<ls_pos name="beq" id="6775"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="beq"/>
</ls_pos>
<ls_pos name="ble" id="6801"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="ble"/>
</ls_pos>
<ls_pos name="bgt" id="6814"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="bgt"/>
</ls_pos>
<ls_pos name="isetvar_pre" id="6883"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="isetvar_pre"/>
</ls_pos>
<ls_pos name="isetvar_post" id="6912"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="isetvar_post"/>
</ls_pos>
<ls_pos name="isetvar_fun" id="6950"
ip_theory="VM_instr_spec">
<ip_library name="specs"/>
<ip_qualid name="isetvar_fun"/>
</ls_pos>
<ls_pos name="aexpr_post" id="7027"
ip_theory="Compile_aexpr">
<ip_qualid name="aexpr_post"/>
</ls_pos>
<ls_pos name="exec_cond" id="8754"
ip_theory="Compile_bexpr">
<ip_qualid name="exec_cond"/>
</ls_pos>
<pr_pos name="Assoc" id="1902"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Unit_def_l" id="1909"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Unit_def_l"/>
</pr_pos>
<pr_pos name="Unit_def_r" id="1912"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Unit_def_r"/>
</pr_pos>
<pr_pos name="Inv_def_l" id="1915"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_l"/>
</pr_pos>
<pr_pos name="Inv_def_r" id="1918"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_r"/>
</pr_pos>
<pr_pos name="Comm" id="1921"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Assoc" id="1926"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Assoc"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Mul_distr_l" id="1933"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_l"/>
</pr_pos>
<pr_pos name="Mul_distr_r" id="1940"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_r"/>
</pr_pos>
<pr_pos name="Comm" id="1958"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Unitary" id="1963"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Unitary"/>
</pr_pos>
<pr_pos name="NonTrivialRing" id="1966"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="NonTrivialRing"/>
</pr_pos>
<pr_pos name="Refl" id="1978"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Refl"/>
</pr_pos>
<pr_pos name="Trans" id="1981"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Trans"/>
</pr_pos>
<pr_pos name="Antisymm" id="1988"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Antisymm"/>
</pr_pos>
<pr_pos name="Total" id="1993"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Total"/>
</pr_pos>
<pr_pos name="ZeroLessOne" id="1998"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="ZeroLessOne"/>
</pr_pos>
<pr_pos name="CompatOrderAdd" id="1999"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderAdd"/>
</pr_pos>
<pr_pos name="CompatOrderMult" id="2006"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderMult"/>
</pr_pos>
<pr_pos name="Abs_le" id="2019"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="Abs_le"/>
</pr_pos>
<pr_pos name="Abs_pos" id="2024"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="Abs_pos"/>
</pr_pos>
<pr_pos name="Div_mod" id="2145"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_mod"/>
</pr_pos>
<pr_pos name="Mod_bound" id="2150"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_bound"/>
</pr_pos>
<pr_pos name="Div_bound" id="2162"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_bound"/>
</pr_pos>
<pr_pos name="Mod_1" id="2167"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_1"/>
</pr_pos>
<pr_pos name="Div_1" id="2170"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_1"/>
</pr_pos>
<pr_pos name="Div_inf" id="2173"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_inf"/>
</pr_pos>
<pr_pos name="Div_inf_neg" id="2178"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_inf_neg"/>
</pr_pos>
<pr_pos name="Mod_0" id="2183"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_0"/>
</pr_pos>
<pr_pos name="Div_1_left" id="2186"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_1_left"/>
</pr_pos>
<pr_pos name="Div_minus1_left" id="2189"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_minus1_left"/>
</pr_pos>
<pr_pos name="Mod_1_left" id="2192"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_1_left"/>
</pr_pos>
<pr_pos name="Mod_minus1_left" id="2195"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_minus1_left"/>
</pr_pos>
<pr_pos name="Div_mult" id="2198"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_mult"/>
</pr_pos>
<pr_pos name="Mod_mult" id="2205"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_mult"/>
</pr_pos>
<pr_pos name="Length_nonnegative" id="2771"
ip_theory="Length">
<ip_library name="list"/>
<ip_qualid name="Length_nonnegative"/>
</pr_pos>
<pr_pos name="Length_nil" id="2774"
ip_theory="Length">
<ip_library name="list"/>
<ip_qualid name="Length_nil"/>
</pr_pos>
<pr_pos name="Append_assoc" id="4157"
ip_theory="Append">
<ip_library name="list"/>
<ip_qualid name="Append_assoc"/>
</pr_pos>
<pr_pos name="Append_l_nil" id="4164"
ip_theory="Append">
<ip_library name="list"/>
<ip_qualid name="Append_l_nil"/>
</pr_pos>
<pr_pos name="Append_length" id="4167"
ip_theory="Append">
<ip_library name="list"/>
<ip_qualid name="Append_length"/>
</pr_pos>