Commit 33f8886f authored by Clément Fumex's avatar Clément Fumex

fix incorrect order of significand and exponent in the case of denormals in Number.compute_float

parent 3d9cd96a
......@@ -6,6 +6,8 @@ theory A
lemma ebsb32 : Float32.t'eb = 8 /\ Float32.t'sb = 24
lemma ebsb64 : Float64.t'eb = 11 /\ Float64.t'sb = 53
goal a : (0.000000000000000000000000000000000000007346836890042368275170461510179868906534397169301663256398154650103540092009879458601062651723623275756835937500:Float32.t) <> (0.0:Float32.t)
end
module M603_018
......
......@@ -9,42 +9,43 @@
<prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../ieee_float.mlw" expanded="true">
<theory name="A" sum="11b8a18803e3f976dcc6f15eacb03d03">
<goal name="ebsb32">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<theory name="A" sum="763d6fbd523a80b8e6b4593a898a6c22" expanded="true">
<goal name="ebsb32" expanded="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="78"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="ebsb64">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<goal name="ebsb64" expanded="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="78"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="a" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="82"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="M603_018" sum="c1f81e18bfb6e6c677b49d1d9f51b22c" expanded="true">
<goal name="WP_parameter triplet" expl="VC for triplet" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter triplet.1" expl="1. assertion" expanded="true">
<goal name="WP_parameter triplet" expl="VC for triplet">
<transf name="split_goal_wp">
<goal name="WP_parameter triplet.1" expl="1. assertion">
<proof prover="3"><result status="valid" time="1.05"/></proof>
<proof prover="4"><result status="valid" time="2.65"/></proof>
</goal>
<goal name="WP_parameter triplet.2" expl="2. assertion" expanded="true">
<goal name="WP_parameter triplet.2" expl="2. assertion">
<proof prover="2"><result status="valid" time="4.95" steps="10731"/></proof>
<proof prover="3"><result status="valid" time="1.86"/></proof>
<proof prover="4"><result status="valid" time="0.79"/></proof>
</goal>
<goal name="WP_parameter triplet.3" expl="3. assertion" expanded="true">
<goal name="WP_parameter triplet.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.64"/></proof>
<proof prover="1"><result status="valid" time="0.21"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="161"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter triplet.4" expl="4. assertion" expanded="true">
<goal name="WP_parameter triplet.4" expl="4. assertion">
<proof prover="0"><result status="outofmemory" time="4.61"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
......@@ -52,17 +53,17 @@
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter triplet.5" expl="5. assertion" expanded="true">
<goal name="WP_parameter triplet.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.64"/></proof>
<proof prover="1"><result status="valid" time="0.29"/></proof>
<proof prover="2"><result status="valid" time="1.13" steps="2244"/></proof>
<proof prover="3"><result status="valid" time="0.62"/></proof>
<proof prover="5"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="WP_parameter triplet.6" expl="6. assertion" expanded="true">
<goal name="WP_parameter triplet.6" expl="6. assertion">
<proof prover="3"><result status="valid" time="2.34"/></proof>
</goal>
<goal name="WP_parameter triplet.7" expl="7. assertion" expanded="true">
<goal name="WP_parameter triplet.7" expl="7. assertion">
<proof prover="0"><result status="valid" time="0.64"/></proof>
<proof prover="1"><result status="valid" time="0.28"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="184"/></proof>
......@@ -70,7 +71,7 @@
<proof prover="4"><result status="valid" time="0.14"/></proof>
<proof prover="5"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="WP_parameter triplet.8" expl="8. assertion" expanded="true">
<goal name="WP_parameter triplet.8" expl="8. assertion">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
......@@ -78,7 +79,7 @@
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter triplet.9" expl="9. assertion" expanded="true">
<goal name="WP_parameter triplet.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="94"/></proof>
......@@ -86,7 +87,7 @@
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter triplet.10" expl="10. assertion" expanded="true">
<goal name="WP_parameter triplet.10" expl="10. assertion">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
......@@ -148,35 +149,35 @@
<theory name="M121_039_nonlinear" sum="419f288237e908f28fe9898d1fbeb90a" expanded="true">
<goal name="WP_parameter test" expl="VC for test" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter test.1" expl="1. assertion" expanded="true">
<goal name="WP_parameter test.1" expl="1. assertion">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter test.2" expl="2. assertion" expanded="true">
<goal name="WP_parameter test.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter test.3" expl="3. assertion" expanded="true">
<goal name="WP_parameter test.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter test.4" expl="4. assertion" expanded="true">
<goal name="WP_parameter test.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter test.5" expl="5. assertion" expanded="true">
<goal name="WP_parameter test.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.15"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="88"/></proof>
......@@ -185,40 +186,34 @@
</goal>
<goal name="WP_parameter test.6" expl="6. assertion" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="unknown" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="valid" time="0.58"/></proof>
<proof prover="5"><result status="unknown" time="4.98"/></proof>
</goal>
<goal name="WP_parameter test.7" expl="7. assertion" expanded="true">
<proof prover="0"><result status="outofmemory" time="4.57"/></proof>
<proof prover="1"><result status="unknown" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="unknown" time="5.00"/></proof>
</goal>
<goal name="WP_parameter test.8" expl="8. assertion" expanded="true">
<proof prover="0"><result status="outofmemory" time="4.43"/></proof>
<proof prover="1"><result status="unknown" time="4.96"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="unknown" time="4.96"/></proof>
</goal>
<goal name="WP_parameter test.9" expl="9. assertion" expanded="true">
<goal name="WP_parameter test.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="91"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter test.10" expl="10. assertion" expanded="true">
<goal name="WP_parameter test.10" expl="10. assertion">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="valid" time="0.17"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="WP_parameter test.11" expl="11. postcondition" expanded="true">
<goal name="WP_parameter test.11" expl="11. postcondition">
<proof prover="0"><result status="outofmemory" time="4.39"/></proof>
<proof prover="1"><result status="unknown" time="4.96"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
......@@ -231,18 +226,16 @@
<theory name="LB09_025_conversion" sum="28457788671e9639392ac3a0fb62e20b" expanded="true">
<goal name="WP_parameter fti" expl="VC for fti" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fti.1" expl="1. postcondition">
<goal name="WP_parameter fti.1" expl="1. postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter fti.2" expl="2. postcondition">
<goal name="WP_parameter fti.2" expl="2. postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter fti.3" expl="3. postcondition">
......
......@@ -412,7 +412,7 @@ let compute_float c fp =
(to_string !s) (to_string (sub emax one)) (print_in_base 2 (Some (to_int eb))) zero
(print_in_base 2 (Some (to_int (sub sb one)))) !s;
!s, zero
zero, !s
end else begin
(* normal case *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment