Commit 9ea9cc34 authored by MARCHE Claude's avatar MARCHE Claude

Bitvector example: more proofs

parent 2098f8e9
......@@ -47,7 +47,7 @@
name="nth_one1"
locfile="bitvectors/double/../double.why"
loclnum="73" loccnumb="8" loccnume="16"
sum="d18ab08209f31f731dfd704613a2e30b"
sum="3848d3fd3fbc40c879e047aaab4a85a2"
proved="true"
expanded="false"
shape="ainfix =anthaoneV0aFalseIainfix <=V0c51Aainfix <=c0V0F">
......@@ -64,7 +64,7 @@
name="nth_one2"
locfile="bitvectors/double/../double.why"
loclnum="74" loccnumb="8" loccnume="16"
sum="dbdf93155a985325f8f4fedd2cc1ce23"
sum="719c2d2317fadc995adafb386c90b2c5"
proved="true"
expanded="false"
shape="ainfix =anthaoneV0aTrueIainfix <=V0c61Aainfix <=c52V0F">
......@@ -74,14 +74,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal
name="nth_one3"
locfile="bitvectors/double/../double.why"
loclnum="75" loccnumb="8" loccnume="16"
sum="78dcef156ce4f14b8c06646563922753"
sum="6778125994116ef0019c84160a720db2"
proved="true"
expanded="false"
shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c63Aainfix &lt;=c62V0F">
......@@ -91,14 +91,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal
name="sign_one"
locfile="bitvectors/double/../double.why"
loclnum="77" loccnumb="8" loccnume="16"
sum="ff5eb7f2e82fa0653ea1884adaa61d9f"
sum="b70858eca86de90b74841ff3d76acfbc"
proved="true"
expanded="false"
shape="ainfix =asignaoneaFalse">
......@@ -108,7 +108,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.12"/>
</proof>
<proof
prover="1"
......@@ -124,7 +124,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
......@@ -132,7 +132,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="5"
......@@ -140,14 +140,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal
name="exp_one"
locfile="bitvectors/double/../double.why"
loclnum="78" loccnumb="8" loccnume="15"
sum="08f27bcd545f7664746d5232bff96501"
sum="15a5f4ba0b6c6193db79d281053be198"
proved="true"
expanded="false"
shape="ainfix =aexpaonec1023">
......@@ -157,7 +157,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="4.87"/>
<result status="valid" time="0.58"/>
</proof>
<proof
prover="3"
......@@ -166,14 +166,14 @@
edited="double_TestDouble_exp_one_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.60"/>
<result status="valid" time="0.66"/>
</proof>
</goal>
<goal
name="mantissa_one"
locfile="bitvectors/double/../double.why"
loclnum="79" loccnumb="8" loccnume="20"
sum="3916c94461ebce50b2aa55917a3011b8"
sum="d8d24976ea1004e5f2a002910f1f0307"
proved="true"
expanded="false"
shape="ainfix =amantissaaonec0">
......@@ -183,7 +183,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.67"/>
<result status="valid" time="0.77"/>
</proof>
<proof
prover="0"
......@@ -199,14 +199,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.98"/>
<result status="valid" time="3.21"/>
</proof>
</goal>
<goal
name="double_value_of_1"
locfile="bitvectors/double/../double.why"
loclnum="81" loccnumb="8" loccnume="25"
sum="d5d64f7ab2d369243a42739379eb07a9"
sum="fef95cf59dfcb5007abf14eb78393ff2"
proved="true"
expanded="false"
shape="ainfix =adouble_of_bv64aonec1.0">
......@@ -216,7 +216,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
......
......@@ -32,7 +32,7 @@
name="Nth_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="13" loccnumb="8" loccnume="13"
sum="abc7eaee768e35d633c1052837f84c8c"
sum="313f7cfd9cb238cefe6b30a61ef11c31"
proved="true"
expanded="false"
shape="ainfix =anthajV0aFalseIainfix &lt;=V0c62Aainfix &lt;=c0V0F">
......@@ -42,14 +42,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
<result status="valid" time="0.09"/>
</proof>
</goal>
<goal
name="sign_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="15" loccnumb="8" loccnume="17"
sum="34eec7200ed8e48eaf94d3cc7620a3dc"
sum="1c5c190d58ac88ccf9f66a6e92798676"
proved="true"
expanded="false"
shape="ainfix =asignajaTrue">
......@@ -66,7 +66,7 @@
name="mantissa_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="16" loccnumb="8" loccnume="21"
sum="6970305c1ef7a17012115ef268945552"
sum="522d8bafdca7f060bd6692b30a154154"
proved="true"
expanded="false"
shape="ainfix =amantissaajc0">
......@@ -76,7 +76,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.66"/>
<result status="valid" time="0.74"/>
</proof>
<proof
prover="0"
......@@ -84,7 +84,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.16"/>
</proof>
<proof
prover="3"
......@@ -92,14 +92,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.40"/>
<result status="valid" time="3.69"/>
</proof>
</goal>
<goal
name="exp_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="17" loccnumb="8" loccnume="16"
sum="8faf4117201f47f3d9a2bbedaae3c556"
sum="8124c943d92944659f01f19ed43f7c04"
proved="true"
expanded="false"
shape="ainfix =aexpajc0">
......@@ -109,7 +109,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.66"/>
<result status="valid" time="0.74"/>
</proof>
<proof
prover="0"
......@@ -117,7 +117,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.16"/>
</proof>
<proof
prover="3"
......@@ -125,14 +125,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.21"/>
<result status="valid" time="3.08"/>
</proof>
</goal>
<goal
name="int_of_bv"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="18" loccnumb="8" loccnume="17"
sum="aa658bdd2ce269f4bcf82983ea27b498"
sum="d341fed6fab8b02bd0bba58deeb31623"
proved="true"
expanded="false"
shape="ainfix =adouble_of_bv64ajc0.0">
......@@ -142,7 +142,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.12"/>
</proof>
<proof
prover="0"
......@@ -158,14 +158,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal
name="MainResultBits"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="20" loccnumb="8" loccnume="22"
sum="03bfc9513d319c9b73254a74d633013c"
sum="9ea8f95e8958d5af3426f01ba4e45dbf"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0ajV1anthV0V1Iainfix &lt;V1c63Aainfix &lt;=c0V1FF">
......@@ -182,7 +182,7 @@
name="MainResultSign"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="23" loccnumb="8" loccnume="22"
sum="4f563eb91bd49148fab0954a7ac4b7a8"
sum="9b95d73cc715f26a6e4a596ad40601a2"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0ajc63anotbanthV0c63F">
......@@ -192,14 +192,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="Sign_of_xor_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="25" loccnumb="8" loccnume="21"
sum="b19c46ce4058940cea14d79fc9d3d0c0"
sum="5c22f51afd72897f2722925bdf3ca2b0"
proved="true"
expanded="false"
shape="ainfix =asignabw_xorV0ajanotbasignV0F">
......@@ -232,7 +232,7 @@
name="Exp_of_xor_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="27" loccnumb="8" loccnume="20"
sum="bf6f51fa79aaec331c331c4b0ebda5dd"
sum="ccbeb8d697184227f9f75d9bacb2a039"
proved="true"
expanded="false"
shape="ainfix =aexpabw_xorV0ajaexpV0F">
......@@ -242,7 +242,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.69"/>
<result status="valid" time="0.76"/>
</proof>
<proof
prover="0"
......@@ -250,7 +250,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.91"/>
<result status="valid" time="0.96"/>
</proof>
<proof
prover="3"
......@@ -258,14 +258,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.16"/>
<result status="valid" time="3.39"/>
</proof>
</goal>
<goal
name="Mantissa_of_xor_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="29" loccnumb="8" loccnume="25"
sum="5742f66ed818a0906e1a42f5abc3f359"
sum="14f714cc419ba2f8a7c89860ce5b945b"
proved="true"
expanded="false"
shape="ainfix =amantissaabw_xorV0ajamantissaV0F">
......@@ -275,7 +275,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.69"/>
<result status="valid" time="0.77"/>
</proof>
<proof
prover="0"
......@@ -283,7 +283,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.56"/>
<result status="valid" time="0.60"/>
</proof>
<proof
prover="3"
......@@ -291,14 +291,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.32"/>
<result status="valid" time="3.58"/>
</proof>
</goal>
<goal
name="MainResultZero"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="31" loccnumb="8" loccnume="22"
sum="921818a19cb7e0dd4adaa3784b678292"
sum="397e23c002ef82f6a4eace3139cc49c2"
proved="true"
expanded="false"
shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix =amantissaV0c0Aainfix =c0aexpV0F">
......@@ -308,7 +308,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.67"/>
<result status="valid" time="1.07"/>
</proof>
<proof
prover="0"
......@@ -316,7 +316,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.72"/>
<result status="valid" time="0.39"/>
</proof>
<proof
prover="3"
......@@ -324,14 +324,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.10"/>
<result status="valid" time="3.58"/>
</proof>
</goal>
<goal
name="sign_neg"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="34" loccnumb="8" loccnume="16"
sum="b54402c83b94259ef155185ddfdf1260"
sum="610aa54b635d7d1565a29d17127341ca"
proved="true"
expanded="false"
shape="ainfix =asign_valueanotbasignV0aprefix -.asign_valueasignV0F">
......@@ -341,14 +341,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.80"/>
<result status="valid" time="0.34"/>
</proof>
</goal>
<goal
name="MainResult"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="36" loccnumb="8" loccnume="18"
sum="fa6f38fbf181f139fbf31b549f4e91ba"
sum="99f2c975165d320981338aa6c0532b76"
proved="true"
expanded="true"
shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix &lt;aexpV0c2047Aainfix &lt;c0aexpV0F">
......@@ -359,7 +359,7 @@
edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.91"/>
<result status="valid" time="1.03"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="power2/why3session.xml">
name="bitvectors/power2/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -36,13 +36,13 @@
expanded="true">
<theory
name="Pow2int"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="1" loccnumb="7" loccnume="14"
verified="false"
expanded="true">
<goal
name="Power_1"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="11" loccnumb="8" loccnume="15"
sum="33bc32635e211600fb0149bbdc4cf0c0"
proved="true"
......@@ -70,7 +70,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
......@@ -91,7 +91,7 @@
</goal>
<goal
name="Power_sum"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="13" loccnumb="8" loccnume="17"
sum="01d41b81dadfb478ff33dc9bdb7d39d1"
proved="true"
......@@ -104,12 +104,12 @@
edited="power2_Pow2int_Power_sum_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.57"/>
<result status="valid" time="0.64"/>
</proof>
</goal>
<goal
name="pow2pos"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="16" loccnumb="8" loccnume="15"
sum="b29b0d96b6d1c61cf88cd8d6542f22be"
proved="true"
......@@ -122,12 +122,12 @@
edited="power2_Pow2int_pow2pos_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.55"/>
<result status="valid" time="0.61"/>
</proof>
</goal>
<goal
name="pow2_0"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="18" loccnumb="8" loccnume="14"
sum="c994e6847b65cec02a9a67a7e1256098"
proved="true"
......@@ -184,7 +184,7 @@
</goal>
<goal
name="pow2_1"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="19" loccnumb="8" loccnume="14"
sum="0b0ec2b029c61974ce68d31d6f97a172"
proved="true"
......@@ -241,7 +241,7 @@
</goal>
<goal
name="pow2_2"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="20" loccnumb="8" loccnume="14"
sum="4f65b737ca06c7a2538ccc1a85cfc646"
proved="true"
......@@ -290,7 +290,7 @@
</goal>
<goal
name="pow2_3"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="21" loccnumb="8" loccnume="14"
sum="a4b54f2d0edef5ff1c8eed3b1f51abdf"
proved="true"
......@@ -318,7 +318,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -339,7 +339,7 @@
</goal>
<goal
name="pow2_4"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="22" loccnumb="8" loccnume="14"
sum="bf783d4854f46bf58b30fa7956ffd130"
proved="true"
......@@ -388,7 +388,7 @@
</goal>
<goal
name="pow2_5"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="23" loccnumb="8" loccnume="14"
sum="43e68e6fad9b81b6d461bdffdfd4adb1"
proved="true"
......@@ -437,7 +437,7 @@
</goal>
<goal
name="pow2_6"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="24" loccnumb="8" loccnume="14"
sum="edc89c31e276d5ffaa0ff0cd08204f48"
proved="true"
......@@ -465,7 +465,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -486,7 +486,7 @@
</goal>
<goal
name="pow2_7"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="25" loccnumb="8" loccnume="14"
sum="f83d53a4545b22268771697dc2c62487"
proved="true"
......@@ -514,7 +514,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
......@@ -535,7 +535,7 @@
</goal>
<goal
name="pow2_8"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="26" loccnumb="8" loccnume="14"
sum="ea2922b4ffd5b891f1846a24141d0834"
proved="true"
......@@ -584,7 +584,7 @@
</goal>
<goal
name="pow2_9"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="27" loccnumb="8" loccnume="14"
sum="f2b729150337fdf74924ab9057b89793"
proved="true"
......@@ -633,7 +633,7 @@
</goal>
<goal
name="pow2_10"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="28" loccnumb="8" loccnume="15"
sum="9e79db755f052e76ecb4becea2b9845d"
proved="true"
......@@ -645,7 +645,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
......@@ -682,7 +682,7 @@
</goal>
<goal
name="pow2_11"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="29" loccnumb="8" loccnume="15"
sum="3950419939a5e90300324e52aea6ef85"
proved="true"
......@@ -726,12 +726,12 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="pow2_12"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="30" loccnumb="8" loccnume="15"
sum="c9ed517871342bec322595770124fe37"
proved="true"
......@@ -743,7 +743,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -780,7 +780,7 @@
</goal>
<goal
name="pow2_13"
locfile="power2/../power2.why"
locfile="bitvectors/power2/../power2.why"
loclnum="31" loccnumb="8" loccnume="15"
sum="f7d72c29f3a98202b0a3be6da33033bf"