Commit 7adfce46 authored by MARCHE Claude's avatar MARCHE Claude

more on bitvectors example

parent f1f6ec36
<?xml version="1.0" encoding="UTF-8"?> <?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 <why3session
name="bitvectors/double_of_int/why3session.xml"> name="double_of_int/why3session.xml">
<prover <prover
id="0" id="0"
name="Alt-Ergo" name="Alt-Ergo"
...@@ -33,16 +33,16 @@ ...@@ -33,16 +33,16 @@
<file <file
name="../double_of_int.why" name="../double_of_int.why"
verified="false" verified="false"
expanded="false"> expanded="true">
<theory <theory
name="DoubleOfInt" name="DoubleOfInt"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="3" loccnumb="7" loccnume="18" loclnum="3" loccnumb="7" loccnume="18"
verified="false" verified="false"
expanded="true"> expanded="true">
<goal <goal
name="jp0_30" name="jp0_30"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="25" loccnumb="8" loccnume="14" loclnum="25" loccnumb="8" loccnume="14"
sum="dd1e1ceb3a9788e30e15fe9c25a9382a" sum="dd1e1ceb3a9788e30e15fe9c25a9382a"
proved="true" proved="true"
...@@ -59,7 +59,7 @@ ...@@ -59,7 +59,7 @@
</goal> </goal>
<goal <goal
name="nth_const1" name="nth_const1"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="41" loccnumb="8" loccnume="18" loclnum="41" loccnumb="8" loccnume="18"
sum="261d6c248d650ec55f76dd63e84bc0e3" sum="261d6c248d650ec55f76dd63e84bc0e3"
proved="true" proved="true"
...@@ -76,7 +76,7 @@ ...@@ -76,7 +76,7 @@
</goal> </goal>
<goal <goal
name="nth_const2" name="nth_const2"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="42" loccnumb="8" loccnume="18" loclnum="42" loccnumb="8" loccnume="18"
sum="daf929e1d75bad068e4657175e1314a0" sum="daf929e1d75bad068e4657175e1314a0"
proved="true" proved="true"
...@@ -93,7 +93,7 @@ ...@@ -93,7 +93,7 @@
</goal> </goal>
<goal <goal
name="nth_const3" name="nth_const3"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="43" loccnumb="8" loccnume="18" loclnum="43" loccnumb="8" loccnume="18"
sum="737f1a2db4422815ed1bc511f8080f23" sum="737f1a2db4422815ed1bc511f8080f23"
proved="true" proved="true"
...@@ -110,7 +110,7 @@ ...@@ -110,7 +110,7 @@
</goal> </goal>
<goal <goal
name="nth_const4" name="nth_const4"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="44" loccnumb="8" loccnume="18" loclnum="44" loccnumb="8" loccnume="18"
sum="182396c90f8ea54cff0a7541d27d6cec" sum="182396c90f8ea54cff0a7541d27d6cec"
proved="true" proved="true"
...@@ -127,7 +127,7 @@ ...@@ -127,7 +127,7 @@
</goal> </goal>
<goal <goal
name="nth_const5" name="nth_const5"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="45" loccnumb="8" loccnume="18" loclnum="45" loccnumb="8" loccnume="18"
sum="1e5b09a5be939521831570ad2a468783" sum="1e5b09a5be939521831570ad2a468783"
proved="true" proved="true"
...@@ -144,7 +144,7 @@ ...@@ -144,7 +144,7 @@
</goal> </goal>
<goal <goal
name="nth_const6" name="nth_const6"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="46" loccnumb="8" loccnume="18" loclnum="46" loccnumb="8" loccnume="18"
sum="22d800cdc6cd6ab8b99dd99bd0b50323" sum="22d800cdc6cd6ab8b99dd99bd0b50323"
proved="true" proved="true"
...@@ -161,7 +161,7 @@ ...@@ -161,7 +161,7 @@
</goal> </goal>
<goal <goal
name="nth_const7" name="nth_const7"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="47" loccnumb="8" loccnume="18" loclnum="47" loccnumb="8" loccnume="18"
sum="f996be957be7f520983d69ddec7a44ef" sum="f996be957be7f520983d69ddec7a44ef"
proved="true" proved="true"
...@@ -178,7 +178,7 @@ ...@@ -178,7 +178,7 @@
</goal> </goal>
<goal <goal
name="nth_const8" name="nth_const8"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="48" loccnumb="8" loccnume="18" loclnum="48" loccnumb="8" loccnume="18"
sum="4c23639c5ec039a10e6e325b1301e497" sum="4c23639c5ec039a10e6e325b1301e497"
proved="true" proved="true"
...@@ -195,7 +195,7 @@ ...@@ -195,7 +195,7 @@
</goal> </goal>
<goal <goal
name="nth_const9" name="nth_const9"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="49" loccnumb="8" loccnume="18" loclnum="49" loccnumb="8" loccnume="18"
sum="f76d9a803bc45a893cca15ce1d3335e8" sum="f76d9a803bc45a893cca15ce1d3335e8"
proved="true" proved="true"
...@@ -212,7 +212,7 @@ ...@@ -212,7 +212,7 @@
</goal> </goal>
<goal <goal
name="sign_const" name="sign_const"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="51" loccnumb="8" loccnume="18" loclnum="51" loccnumb="8" loccnume="18"
sum="e7060da582f6a712f7fd94be17f80dd0" sum="e7060da582f6a712f7fd94be17f80dd0"
proved="true" proved="true"
...@@ -269,7 +269,7 @@ ...@@ -269,7 +269,7 @@
</goal> </goal>
<goal <goal
name="exp_const" name="exp_const"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="53" loccnumb="8" loccnume="17" loclnum="53" loccnumb="8" loccnume="17"
sum="5c5372a8718de21456f67bd1ca4d0307" sum="5c5372a8718de21456f67bd1ca4d0307"
proved="true" proved="true"
...@@ -287,7 +287,7 @@ ...@@ -287,7 +287,7 @@
</goal> </goal>
<goal <goal
name="to_nat_mantissa_1" name="to_nat_mantissa_1"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="55" loccnumb="8" loccnume="25" loclnum="55" loccnumb="8" loccnume="25"
sum="1fa1973374d4d12946d36e021270b22f" sum="1fa1973374d4d12946d36e021270b22f"
proved="true" proved="true"
...@@ -320,7 +320,7 @@ ...@@ -320,7 +320,7 @@
</goal> </goal>
<goal <goal
name="mantissa_const_nth2" name="mantissa_const_nth2"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="57" loccnumb="8" loccnume="27" loclnum="57" loccnumb="8" loccnume="27"
sum="7433d00332d59717c1ffdf7ec45114f3" sum="7433d00332d59717c1ffdf7ec45114f3"
proved="true" proved="true"
...@@ -369,7 +369,7 @@ ...@@ -369,7 +369,7 @@
</goal> </goal>
<goal <goal
name="mantissa_const_to_nat51" name="mantissa_const_to_nat51"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="60" loccnumb="8" loccnume="31" loclnum="60" loccnumb="8" loccnume="31"
sum="50e2e6714169744021a05e4814b9dc09" sum="50e2e6714169744021a05e4814b9dc09"
proved="true" proved="true"
...@@ -402,7 +402,7 @@ ...@@ -402,7 +402,7 @@
</goal> </goal>
<goal <goal
name="mantissa_const" name="mantissa_const"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="63" loccnumb="8" loccnume="22" loclnum="63" loccnumb="8" loccnume="22"
sum="2ff85bcb325502fbe7940125d2f49870" sum="2ff85bcb325502fbe7940125d2f49870"
proved="true" proved="true"
...@@ -435,7 +435,7 @@ ...@@ -435,7 +435,7 @@
</goal> </goal>
<goal <goal
name="real1075m1023" name="real1075m1023"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="65" loccnumb="8" loccnume="21" loclnum="65" loccnumb="8" loccnume="21"
sum="a8ea52f2a5b6aeabdde75cd427b9b403" sum="a8ea52f2a5b6aeabdde75cd427b9b403"
proved="true" proved="true"
...@@ -484,7 +484,7 @@ ...@@ -484,7 +484,7 @@
</goal> </goal>
<goal <goal
name="real1075m1023_2" name="real1075m1023_2"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="67" loccnumb="8" loccnume="23" loclnum="67" loccnumb="8" loccnume="23"
sum="ef4f676fc3549cdde4e75e5d1a3bca21" sum="ef4f676fc3549cdde4e75e5d1a3bca21"
proved="true" proved="true"
...@@ -541,48 +541,24 @@ ...@@ -541,48 +541,24 @@
</goal> </goal>
<goal <goal
name="real52_a_m52" name="real52_a_m52"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="69" loccnumb="8" loccnume="20" loclnum="69" loccnumb="8" loccnume="20"
sum="091e7b7b8d42964e6fc2897ac38606c8" sum="091e7b7b8d42964e6fc2897ac38606c8"
proved="false" proved="true"
expanded="true" expanded="false"
shape="ainfix =ainfix *.ainfix *.apow2ainfix -c1075c1023apow2c31apow2aprefix -c52apow2c31"> shape="ainfix =ainfix *.ainfix *.apow2ainfix -c1075c1023apow2c31apow2aprefix -c52apow2c31">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof <proof
prover="0" prover="0"
timelimit="5" timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="timeout" time="5.01"/> <result status="valid" time="11.12"/>
</proof> </proof>
</goal> </goal>
<goal <goal
name="const_value0" name="const_value0"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="71" loccnumb="8" loccnume="20" loclnum="71" loccnumb="8" loccnume="20"
sum="053e10e406e6f3b38b72aece1d2ea1cc" sum="053e10e406e6f3b38b72aece1d2ea1cc"
proved="true" proved="true"
...@@ -615,7 +591,7 @@ ...@@ -615,7 +591,7 @@
</goal> </goal>
<goal <goal
name="const_value" name="const_value"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="74" loccnumb="8" loccnume="19" loclnum="74" loccnumb="8" loccnume="19"
sum="15c0e266eaa7e83629a4b99a8c7fbbbc" sum="15c0e266eaa7e83629a4b99a8c7fbbbc"
proved="true" proved="true"
...@@ -656,7 +632,7 @@ ...@@ -656,7 +632,7 @@
</goal> </goal>
<goal <goal
name="nth_0_30" name="nth_0_30"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="100" loccnumb="8" loccnume="16" loclnum="100" loccnumb="8" loccnume="16"
sum="0f62d85765410f7e4511d07bde414f6b" sum="0f62d85765410f7e4511d07bde414f6b"
proved="true" proved="true"
...@@ -689,7 +665,7 @@ ...@@ -689,7 +665,7 @@
</goal> </goal>
<goal <goal
name="nth_jpxor_0_30" name="nth_jpxor_0_30"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="102" loccnumb="8" loccnume="22" loclnum="102" loccnumb="8" loccnume="22"
sum="122538c45d56e139bb3836e5a0df1b67" sum="122538c45d56e139bb3836e5a0df1b67"
proved="true" proved="true"
...@@ -722,7 +698,7 @@ ...@@ -722,7 +698,7 @@
</goal> </goal>
<goal <goal
name="nth_var31" name="nth_var31"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="104" loccnumb="8" loccnume="17" loclnum="104" loccnumb="8" loccnume="17"
sum="615ab90161692c1aeedf9d5b18404b7b" sum="615ab90161692c1aeedf9d5b18404b7b"
proved="true" proved="true"
...@@ -739,7 +715,7 @@ ...@@ -739,7 +715,7 @@
</goal> </goal>
<goal <goal
name="to_nat_sub_0_30" name="to_nat_sub_0_30"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="107" loccnumb="8" loccnume="23" loclnum="107" loccnumb="8" loccnume="23"
sum="dfb01a9181d5c0966a7d6ec96d5ac09b" sum="dfb01a9181d5c0966a7d6ec96d5ac09b"
proved="true" proved="true"
...@@ -780,7 +756,7 @@ ...@@ -780,7 +756,7 @@
</goal> </goal>
<goal <goal
name="jpxorx_pos" name="jpxorx_pos"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="114" loccnumb="8" loccnume="18" loclnum="114" loccnumb="8" loccnume="18"
sum="44892484235e0bcc9ae0ae2692013aa4" sum="44892484235e0bcc9ae0ae2692013aa4"
proved="true" proved="true"
...@@ -829,7 +805,7 @@ ...@@ -829,7 +805,7 @@
</goal> </goal>
<goal <goal
name="from_int2c_to_nat_sub_gen" name="from_int2c_to_nat_sub_gen"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="121" loccnumb="8" loccnume="33" loclnum="121" loccnumb="8" loccnume="33"
sum="5ebb2305fcfec2d2956b80a9e1b8fb25" sum="5ebb2305fcfec2d2956b80a9e1b8fb25"
proved="false" proved="false"
...@@ -859,10 +835,19 @@ ...@@ -859,10 +835,19 @@
archived="false"> archived="false">
<result status="timeout" time="5.02"/> <result status="timeout" time="5.02"/>
</proof> </proof>
<proof
prover="3"
timelimit="30"
memlimit="1000"
edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_gen_1.v"
obsolete="false"
archived="false">
<result status="unknown" time="1.82"/>
</proof>
</goal> </goal>
<goal <goal
name="from_int2c_to_nat_sub" name="from_int2c_to_nat_sub"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="126" loccnumb="8" loccnume="29" loclnum="126" loccnumb="8" loccnume="29"
sum="ad558127c1887d36861533f052fa7881" sum="ad558127c1887d36861533f052fa7881"
proved="false" proved="false"
...@@ -870,32 +855,48 @@ ...@@ -870,32 +855,48 @@
shape="ainfix =ato_nat_subafrom_int2cV0c30c0V0Iainfix &gt;=V0c0Aais_int32V0F"> shape="ainfix =ato_nat_subafrom_int2cV0c30c0V0Iainfix &gt;=V0c0Aais_int32V0F">
<proof <proof
prover="5" prover="5"
timelimit="5" timelimit="30"
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="timeout" time="5.12"/> <result status="highfailure" time="13.35"/>
</proof>
<proof
prover="1"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="0.19"/>
</proof> </proof>
<proof <proof
prover="0" prover="0"
timelimit="5" timelimit="30"
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="timeout" time="5.02"/> <result status="timeout" time="30.10"/>
</proof>
<proof
prover="2"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="0.42"/>
</proof> </proof>
<proof <proof
prover="6" prover="6"
timelimit="5" timelimit="30"
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="timeout" time="5.02"/> <result status="highfailure" time="17.06"/>
</proof> </proof>
</goal> </goal>
<goal <goal
name="lemma1_pos" name="lemma1_pos"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="129" loccnumb="8" loccnume="18" loclnum="129" loccnumb="8" loccnume="18"
sum="d139a96e73e962725d19413c55cb8b14" sum="d139a96e73e962725d19413c55cb8b14"
proved="false" proved="false"
...@@ -928,7 +929,7 @@ ...@@ -928,7 +929,7 @@
</goal> </goal>
<goal <goal
name="to_nat_sub_0_30_neg" name="to_nat_sub_0_30_neg"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="133" loccnumb="8" loccnume="27" loclnum="133" loccnumb="8" loccnume="27"
sum="99070120f3f44a6f210fea6e47536165" sum="99070120f3f44a6f210fea6e47536165"
proved="true" proved="true"
...@@ -977,7 +978,7 @@ ...@@ -977,7 +978,7 @@
</goal> </goal>
<goal <goal
name="to_nat_sub_0_30_neg1" name="to_nat_sub_0_30_neg1"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="136" loccnumb="8" loccnume="28" loclnum="136" loccnumb="8" loccnume="28"
sum="7700539e32b8c609dda46df0274b2fa4" sum="7700539e32b8c609dda46df0274b2fa4"
proved="false" proved="false"
...@@ -1010,40 +1011,24 @@ ...@@ -1010,40 +1011,24 @@
</goal> </goal>
<goal <goal
name="lemma1_neg" name="lemma1_neg"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="139" loccnumb="8" loccnume="18" loclnum="139" loccnumb="8" loccnume="18"
sum="f9b7369b8893d642cfe764d5817e2a95" sum="f9b7369b8893d642cfe764d5817e2a95"
proved="false" proved="true"
expanded="true" expanded="false"
shape="ainfix =ato_nat_subajpxorV0c31c0ainfix +apow2c31V0Iainfix &lt;V0c0Aais_int32V0F"> shape="ainfix =ato_nat_subajpxorV0c31c0ainfix +apow2c31V0Iainfix &lt;V0c0Aais_int32V0F">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof <proof
prover="6" prover="6"
timelimit="5" timelimit="30"
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="timeout" time="5.02"/> <result status="valid" time="17.02"/>
</proof> </proof>
</goal> </goal>
<goal <goal
name="lemma1" name="lemma1"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"
loclnum="143" loccnumb="8" loccnume="14" loclnum="143" loccnumb="8" loccnume="14"
sum="e5436643ae8166e1886bbfc73bcef98e" sum="e5436643ae8166e1886bbfc73bcef98e"
proved="true" proved="true"
...@@ -1092,7 +1077,7 @@ ...@@ -1092,7 +1077,7 @@
</goal> </goal>
<goal <goal
name="nth_var_0_31" name="nth_var_0_31"
locfile="bitvectors/double_of_int/../double_of_int.why" locfile="double_of_int/../double_of_int.why"