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

Cleaning and factorization of floating-point support

parent 8e7738c7
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<why3session
name="bts/12475/why3session.xml">
<prover
......@@ -34,7 +34,7 @@
name="toto"
locfile="bts/12475/../12475.why"
loclnum="6" loccnumb="7" loccnume="11"
sum="5dfb61fb4e47918e08b6c1345d16fd44"
sum="9277e7312956b5e244f4586258a899ba"
proved="true"
expanded="true"
shape="ainfix &lt;V0ainfix +aroundaUpV0c1.F">
......@@ -44,7 +44,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -52,7 +52,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
......@@ -60,7 +60,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
......@@ -68,7 +68,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<why3session
name="check-builtin/floats/why3session.xml">
<prover
......@@ -32,7 +32,7 @@
name="Round_single_01"
locfile="check-builtin/floats/../floats.why"
loclnum="11" loccnumb="7" loccnume="22"
sum="88a4c1b2a6f1f03b9b71187a7948ae7e"
sum="8d5596f1dc7557ed743fea14f397c3bb"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
......@@ -49,7 +49,7 @@
name="Round_double_01"
locfile="check-builtin/floats/../floats.why"
loclnum="14" loccnumb="7" loccnume="22"
sum="0a6c684833c7b3a0d8f1d2a061ac45f2"
sum="32107838e0e998b61d3694c4f5f0009f"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
......@@ -66,7 +66,7 @@
name="Test00"
locfile="check-builtin/floats/../floats.why"
loclnum="17" loccnumb="8" loccnume="14"
sum="e10e2f63ebfa7211f99fd93fb8668224"
sum="cd281225d4d500e7379dc6138cd16330"
proved="true"
expanded="true"
shape="ainfix &lt;=aprefix -c3.0V0Iainfix &lt;=aabsV0c2.0F">
......@@ -76,7 +76,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="1"
......@@ -84,7 +84,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="0"
......@@ -92,7 +92,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
......@@ -107,7 +107,7 @@
name="Test01"
locfile="check-builtin/floats/../floats.why"
loclnum="19" loccnumb="8" loccnume="14"
sum="949ba5363a6813ffe06e7bd91be480d1"
sum="86dad2fc6873ddc0073bc0115e52c724"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix &lt;=avalueV0c2.0Aainfix &lt;=aprefix -c2.0avalueV0F">
......@@ -117,14 +117,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Test02"
locfile="check-builtin/floats/../floats.why"
loclnum="25" loccnumb="8" loccnume="14"
sum="4ee75f555811c9d0578eca5d2648e9a9"
sum="ac5095b33417c8bd32759846e5fb4881"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix &lt;=aabsavalueV0c2.0F">
......@@ -134,14 +134,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Test03"
locfile="check-builtin/floats/../floats.why"
loclnum="32" loccnumb="8" loccnume="14"
sum="828c16f3f01245a9009cde43d67acb31"
sum="41a813fab58ad82dd738ec1203c67376"
proved="true"
expanded="true"
shape="ainfix &lt;=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix &lt;=aabsavalueV0c2.0F">
......@@ -151,7 +151,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<why3session
name="./my_cosine/why3session.xml">
<prover
......@@ -9,7 +9,7 @@
<prover
id="1"
name="Coq"
version="8.3pl4"/>
version="8.3pl3"/>
<prover
id="2"
name="Gappa"
......@@ -28,25 +28,25 @@
name="MethodError"
locfile="./my_cosine/../my_cosine.why"
loclnum="13" loccnumb="6" loccnume="17"
sum="afd23768ec9edf61452c5636b149ac05"
sum="1e22c4edd1067353283e8362ea67fdf0"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix &lt;=aabsV0c0x1.p-5F">
<proof
prover="1"
timelimit="10"
timelimit="13"
memlimit="0"
edited="my_cosine_CosineSingle_MethodError_1.v"
obsolete="false"
archived="false">
<result status="valid" time="4.24"/>
<result status="valid" time="6.37"/>
</proof>
</goal>
<goal
name="TotalErrorFullyExpanded"
locfile="./my_cosine/../my_cosine.why"
loclnum="20" loccnumb="6" loccnume="29"
sum="c02ee18e73dfc48ba9c3ce80efd9a7b4"
sum="aadcb6c321ae62976144a46205babd78"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix =V3aroundaNearestTiesToEvenainfix -c1.0V2Iainfix =V2aroundaNearestTiesToEvenainfix *c0.5V1Iainfix =V1aroundaNearestTiesToEvenainfix *avalueV0avalueV0FIainfix &lt;=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *avalueV0avalueV0acosavalueV0c0x1.p-24Iainfix &lt;=aabsavalueV0c0x1.p-5F">
......@@ -56,31 +56,31 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="TotalErrorExpanded"
locfile="./my_cosine/../my_cosine.why"
loclnum="31" loccnumb="6" loccnume="24"
sum="bb822ccd5541b837fdc4a31d2b797d10"
sum="d021d9680b1e11e1aa2c83fdd3c36d71"
proved="true"
expanded="true"
shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix &lt;=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix &lt;=aabsavalueV0c0x1.p-5F">
<proof
prover="0"
timelimit="2"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.86"/>
<result status="valid" time="1.22"/>
</proof>
</goal>
<goal
name="TotalError"
locfile="./my_cosine/../my_cosine.why"
loclnum="51" loccnumb="6" loccnume="16"
sum="4dff1f87fd4812761c9f67528ad45306"
sum="0d725bd8aa56715a6b6f3b5bc0299292"
proved="true"
expanded="true"
shape="Lacos_singleV0ainfix &lt;=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix &lt;=aabsavalueV0c0x1.p-5F">
......@@ -90,7 +90,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="3.27"/>
<result status="valid" time="4.53"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<why3session
name="programs/my_cosine/why3session.xml">
<prover
id="0"
name="Coq"
version="8.3pl4"/>
version="8.3pl3"/>
<prover
id="1"
name="Gappa"
......@@ -25,7 +25,7 @@
locfile="programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="parameter my_cosine"
sum="8c5ef4e174040dfc2edbec12b7ad11c9"
sum="613554e5135277438089d8ff16551aa7"
proved="true"
expanded="true"
shape="ainfix &lt;=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FAainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -40,7 +40,7 @@
locfile="programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="assertion"
sum="f19d8615cb5c434b8497ae0d46cb1e88"
sum="11c4f7c81d63da1453654b5cd6ff0639"
proved="true"
expanded="true"
shape="ainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -48,12 +48,12 @@
name="expl:parameter my_cosine"/>
<proof
prover="0"
timelimit="9"
timelimit="12"
memlimit="0"
edited="my_cosine_M_WP_parameter_my_cosine_1.v"
obsolete="false"
archived="false">
<result status="valid" time="4.51"/>
<result status="valid" time="5.96"/>
</proof>
</goal>
<goal
......@@ -61,7 +61,7 @@
locfile="programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="precondition"
sum="13fda2c30862d2282aa50e9f3aed5e61"
sum="12de20c84831e31ca300cde9629492ff"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -81,7 +81,7 @@
locfile="programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="precondition"
sum="83faf9aa4fd66bb3090a0e3a03bfb095"
sum="8347c5ae52a7c23d8b25cc34f50df355"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -101,7 +101,7 @@
locfile="programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="precondition"
sum="c2a58280312e1542c64994f3bab49f6b"
sum="084afefdd4400a264223024aa7592dfd"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -113,7 +113,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -121,7 +121,7 @@
locfile="programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="normal postcondition"
sum="fb20bbbd761cb5dae33e358483e311a4"
sum="d7405fa3fbaf989f038a1aa69e408d76"
proved="true"
expanded="true"
shape="ainfix &lt;=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -133,7 +133,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<why3session
name="tests-provers/gappa/why3session.xml">
<prover
......@@ -20,7 +20,7 @@
name="Round_single_01"
locfile="tests-provers/gappa/../gappa.why"
loclnum="11" loccnumb="8" loccnume="23"
sum="88a4c1b2a6f1f03b9b71187a7948ae7e"
sum="8d5596f1dc7557ed743fea14f397c3bb"
proved="true"
expanded="false"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
......@@ -37,7 +37,7 @@
name="Round_double_01"
locfile="tests-provers/gappa/../gappa.why"
loclnum="14" loccnumb="8" loccnume="23"
sum="ab93931e6d3e9345694665893e409937"
sum="0364393cc059ccdb3de99dd40d7cdf06"
proved="true"
expanded="false"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
......@@ -54,7 +54,7 @@
name="Test00"
locfile="tests-provers/gappa/../gappa.why"
loclnum="17" loccnumb="9" loccnume="15"
sum="74c33ad8cd506568513aa26005254d2e"
sum="6bb1cae38eba2a75a66592be762b428b"
proved="true"
expanded="false"
shape="ainfix &lt;=aprefix -c3.0V0Iainfix &lt;=aabsV0c2.0F">
......@@ -64,14 +64,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Test01"
locfile="tests-provers/gappa/../gappa.why"
loclnum="19" loccnumb="9" loccnume="15"
sum="077ea61dc71ee8b01e0f6c48cf663e23"
sum="5e3913f891b4a3baa2e8da1305e17f47"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix &lt;=avalueV0c2.0Aainfix &lt;=aprefix -c2.0avalueV0F">
......@@ -81,14 +81,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Test02"
locfile="tests-provers/gappa/../gappa.why"
loclnum="25" loccnumb="9" loccnume="15"
sum="f91cd881f018901a09d72a0c2d30043a"
sum="c99b9e0886cc50bbd89f03d161e8da45"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix &lt;=aabsavalueV0c2.0F">
......@@ -105,7 +105,7 @@
name="Test03"
locfile="tests-provers/gappa/../gappa.why"
loclnum="32" loccnumb="9" loccnume="15"
sum="6deb20cf0dd23b46d4448bf086b03c9f"
sum="d60812e0448110f0c19061c777138b40"
proved="true"
expanded="false"
shape="ainfix &lt;=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix &lt;=aabsavalueV0c2.0F">
......@@ -115,7 +115,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......@@ -129,7 +129,7 @@
name="Test1"
locfile="tests-provers/gappa/../gappa.why"
loclnum="53" loccnumb="8" loccnume="13"
sum="7c3643c0218b539e01ad70a84c96c00f"
sum="780586c907131af3a8db711ff1bc314f"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -avalueaac0.1c0x1.p-53Iainfix =aaarIainfix =avalueararoundaNearestTiesToEvenc0.1">
......@@ -146,7 +146,7 @@
name="Test2"
locfile="tests-provers/gappa/../gappa.why"
loclnum="58" loccnumb="8" loccnume="13"
sum="7348134b45fa87387c002f44cc429e23"
sum="015ec5f2fb0c5fd25bd7b466a94304d7"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -avalueafc0c0.1c0x1.p-53Iainfix =afc0arIainfix =avalueararoundaNearestTiesToEvenc0.1">
......@@ -156,14 +156,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Test3"
locfile="tests-provers/gappa/../gappa.why"
loclnum="63" loccnumb="8" loccnume="13"
sum="4216386f1789302fc7efe39640461d16"
sum="50182d48e211aae23d117c1ad6c2b06b"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -avalueagc0c1c0.1c0x1.p-53Iainfix =agc0c1arIainfix =avalueararoundaNearestTiesToEvenc0.1">
......@@ -173,7 +173,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
......@@ -187,7 +187,7 @@
name="G1"
locfile="tests-provers/gappa/../gappa.why"
loclnum="89" loccnumb="7" loccnume="9"
sum="86dd886e59b47d83acfa5f20a5d53541"
sum="28d9a8aaf749577fce6cee6e8d4b3192"
proved="true"
expanded="true"
shape="ainfix &lt;=ainfix -avaluearesultainfix *avalueaq1avalueaq2c0x1.p-52">
......@@ -197,14 +197,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="G2"
locfile="tests-provers/gappa/../gappa.why"
loclnum="91" loccnumb="7" loccnume="9"
sum="b352c9d926a1495be9c61e61fb69459f"
sum="698acd79137ddd7dd8d1505a38c1e983"
proved="true"
expanded="true"
shape="ainfix &lt;=ainfix -avalueV0ainfix *avalueaq1avalueaq2c0x1.p-52Iainfix =V0aresultF">
......@@ -214,14 +214,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="G3"
locfile="tests-provers/gappa/../gappa.why"
loclnum="94" loccnumb="7" loccnume="9"
sum="33ce3abcfd82832aadf9f843a46116bb"
sum="971eea20fcf064886923dae3a1ab58bf"
proved="true"
expanded="true"
shape="ainfix &lt;=ainfix -avalueV0ainfix *avalueaq1avalueaq2c0x1.p-52Iainfix =V0aresultF">
......
......@@ -14,7 +14,7 @@ theory Rounding
end
(** {2 Handling of IEEE-754 special values}
(** {2 Handling of IEEE-754 special values}
Special values are +infinity, -infinity, NaN, +0, -0. These are
handled as described in {h <a
......@@ -105,6 +105,48 @@ theory GenFloat
end
theory GenFloatSpecStrict
use import Rounding
use import real.Real
clone export GenFloat
(** {3 binary operations} *)
predicate add_post (m:mode) (x y res:t) =
value res = round m (value x + value y) /\
exact res = exact x + exact y /\
model res = model x + model y
predicate sub_post (m:mode) (x y res:t) =
value res = round m (value x - value y) /\
exact res = exact x - exact y /\
model res = model x - model y
predicate mul_post (m:mode) (x y res:t) =
value res = round m (value x * value y) /\
exact res = exact x * exact y /\
model res = model x * model y
predicate div_post (m:mode) (x y res:t) =
value res = round m (value x / value y) /\
exact res = exact x / exact y /\
model res = model x / model y
predicate neg_post (x res:t) =
value res = - value x /\
exact res = - exact x /\
model res = - model x
(** {3 Comparisons} *)
use import bool.Bool
predicate lt_post (x:t) (y:t) (r:bool) =
if r = True then value x < value y else value x >= value y
end
(** {2 Single precision floats}
A.k.a. binary32 numbers.
......@@ -118,7 +160,7 @@ theory Single
constant max_single : real = 0x1.FFFFFEp127
constant max_int : int = 16777216 (* 2^24 *)
clone export GenFloat with
clone export GenFloatSpecStrict with
type t = single,
constant max = max_single,
constant max_representable_integer = max_int
......@@ -138,7 +180,7 @@ theory Double
constant max_double : real = 0x1.FFFFFFFFFFFFFp1023
constant max_int : int = 9007199254740992 (* 2^53 *)
clone export GenFloat with
clone export GenFloatSpecStrict with
type t = double,
constant max = max_double,
constant max_representable_integer = max_int
......@@ -159,7 +201,7 @@ theory GenFloatFull
clone export GenFloat
(** special values *)
(** {3 special values} *)
function class t : class
predicate is_finite (x:t) = class x = Finite
......@@ -172,6 +214,14 @@ theory GenFloatFull
function sign t : sign
predicate same_sign (x:t) (y:t) = sign x = sign y
predicate diff_sign (x:t) (y:t) = sign x <> sign y
predicate sign_zero_result (m:mode) (x:t) =
value x = 0.0 ->
match m with
| Down -> sign x = Neg
| _ -> sign x = Pos
end
predicate is_minus_infinity (x:t) = is_infinite x /\ sign x = Neg
predicate is_plus_infinity (x:t) = is_infinite x /\ sign x = Pos
......@@ -179,6 +229,26 @@ theory GenFloatFull
predicate is_gen_zero_plus (x:t) = is_gen_zero x /\ sign x = Pos
predicate is_gen_zero_minus (x:t) = is_gen_zero x /\ sign x = Neg
(** {3 overflow} *)
(** This predicate tells what is the result of a rounding in case
of overflow *)
predicate overflow_value (m:mode) (x:t) =
match m, sign x with
| Down, Neg -> is_infinite x
| Down, Pos -> is_finite x /\ value x = max
| Up, Neg -> is_finite x /\ value x = - max
| Up, Pos -> is_infinite x
| ToZero, Neg -> is_finite x /\ value x = - max
| ToZero, Pos -> is_finite x /\ value x = max
| (NearestTiesToAway | NearestTiesToEven), _ -> is_infinite x
end
(** {3 binary operations} *)
(** {3 Comparisons} *)
predicate le_full (x:t) (y:t) =
(is_finite x /\ is_finite y /\ value x <= value y)
\/ (is_minus_infinity x /\ is_not_NaN y)
......@@ -217,6 +287,103 @@ theory GenFloatFull
end
theory GenFloatSpecFull
use import real.Real
use import Rounding
use import SpecialValues
clone export GenFloatFull
(** {3 binary operations} *)
predicate add_post (m:mode) (x:t) (y:t) (r:t) =
(is_NaN x \/ is_NaN y -> is_NaN r)
/\
(is_finite x /\ is_infinite y -> is_infinite r /\ same_sign r y)
/\
(is_infinite x /\ is_finite y -> is_infinite r /\ same_sign r x)
/\
(is_infinite x /\ is_infinite y /\ same_sign x y
-> is_infinite r /\ same_sign r x)
/\
(is_infinite x /\ is_infinite y /\ diff_sign x y -> is_NaN r)
/\
(is_finite x /\ is_finite y /\ no_overflow m (value x + value y)
-> is_finite r /\
value r = round m (value x + value y) /\
sign_zero_result m r)
/\
(is_finite x /\ is_finite y /\ not no_overflow m (value x + value y)
-> SpecialValues.same_sign_real (sign r) (value x + value y)
/\ overflow_value m r)
/\ exact r = exact x + exact y
/\ model r = model x + model y
predicate sub_post (m:mode) (x:t) (y:t) (r:t) =
(is_NaN x \/ is_NaN y -> is_NaN r)
/\
(is_finite x /\ is_infinite y -> is_infinite r /\ diff_sign r y)
/\
(is_infinite x /\ is_finite y -> is_infinite r /\ same_sign r x)
/\
(is_infinite x /\ is_infinite y /\ same_sign x y -> is_NaN r)
/\
(is_infinite x /\ is_infinite y /\ diff_sign x y
-> is_infinite r /\ same_sign r x)
/\
(is_finite x /\ is_finite y /\ no_overflow m (value x - value y)
-> is_finite r /\
value r = round m (value x - value y) /\
sign_zero_result m r)
/\
(is_finite x /\ is_finite y /\ not no_overflow m (value x - value y)
-> SpecialValues.same_sign_real (sign r) (value x - value y)
/\ overflow_value m r)
/\ exact r = exact x - exact y
/\ model r = model x - model y
predicate product_sign (z x y: t) =
(same_sign x y -> sign z = Pos) /\ (diff_sign x y -> sign z = Neg)
predicate mul_post (m:mode) (x:t) (y:t) (r:t) =
(is_NaN x \/ is_NaN y -> is_NaN r)
/\ (is_gen_zero x /\ is_infinite y -> is_NaN r)
/\ (is_finite x /\ is_infinite y /\ value x <> 0.0
-> is_infinite r)
/\ (is_infinite x /\ is_gen_zero y -> is_NaN r)
/\ (is_infinite x /\ is_finite y /\ value y <> 0.0
-> is_infinite r)
/\ (is_infinite x /\ is_infinite y -> is_infinite r)
/\ (is_finite x /\ is_finite y /\ no_overflow m (value x * value y)
-> is_finite r /\ value r = round m (value x * value y))
/\ (is_finite x /\ is_finite y /\ not no_overflow m (value x * value y)
-> overflow_value m r)
/\ product_sign r x y
/\ exact r = exact x * exact y
/\ model r = model x * model y
predicate neg_post (x:t) (r:t) =
(is_NaN x -> is_NaN r)
/\ (is_infinite x -> is_infinite r)
/\ (is_finite x -> is_finite r /\ value r = - value x)
/\ diff_sign r x
/\ exact r = - exact x
/\ model r = - model x
predicate of_real_exact_post (x:real) (r:t) =
is_finite r /\ value r = x /\ exact r = x /\ model r = x
(** {3 Comparisons} *)
use import bool.Bool
predicate lt_post (x:t) (y:t) (r:bool) =
if r = True then lt_full x y else not (lt_full x y)
end
(** {2 Full theory of single precision floats} *)
theory SingleFull
......@@ -226,7 +393,7 @@ theory SingleFull