Commit f44d8621 authored by Clément Fumex's avatar Clément Fumex

small changes in bitvector drivers

parent b77a7131
......@@ -22,6 +22,26 @@ theory bv.BV_Gen
(* Warning: we should NOT remove all the axioms using "allprops" *)
remove prop nth_out_of_bound
remove prop Nth_zero
remove prop Nth_ones
remove prop two_power_size_val
remove prop max_int_val
remove prop eq_sub_equiv
remove prop Nth_bw_or
remove prop Nth_bw_and
remove prop Nth_bw_xor
remove prop Nth_bw_not
remove prop Nth_rotate_left
remove prop Nth_rotate_right
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_int_extensionality
remove prop Of_int_zero
remove prop Of_int_ones
remove prop to_uint_add
remove prop to_uint_add_bounded
remove prop to_uint_sub
......@@ -31,16 +51,9 @@ theory bv.BV_Gen
remove prop to_uint_mul_bounded
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
remove prop lsr_bv_is_lsr
remove prop to_uint_lsr
remove prop asr_bv_is_asr
remove prop lsl_bv_is_lsl
remove prop to_uint_lsl
remove prop rotate_left_bv_is_rotate_left
remove prop rotate_right_bv_is_rotate_right
remove prop Extensionality
syntax predicate ult "(bvult %1 %2)"
......
......@@ -82,19 +82,31 @@ end
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
......@@ -25,7 +25,7 @@
<proof prover="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter nth_ultpre0.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.47" steps="210"/></proof>
<proof prover="0"><result status="valid" time="0.52" steps="210"/></proof>
<proof prover="6"><result status="valid" time="0.30"/></proof>
</goal>
</transf>
......@@ -61,7 +61,7 @@
</goal>
<goal name="WP_parameter poke_64bit_bv.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.34" steps="188"/></proof>
<proof prover="6"><result status="valid" time="0.08"/></proof>
<proof prover="6"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.29" steps="163"/></proof>
......@@ -121,7 +121,7 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter peek_8bit_bv.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="1.46" steps="611"/></proof>
<proof prover="0"><result status="valid" time="1.56" steps="611"/></proof>
</goal>
</transf>
</goal>
......@@ -214,7 +214,7 @@
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter peek.13" expl="13. precondition">
<proof prover="3"><result status="valid" time="0.67"/></proof>
<proof prover="3"><result status="valid" time="0.72"/></proof>
</goal>
<goal name="WP_parameter peek.14" expl="14. precondition">
<proof prover="0"><result status="valid" time="0.10" steps="96"/></proof>
......@@ -231,14 +231,14 @@
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter peek.17" expl="17. loop invariant preservation">
<proof prover="4"><result status="valid" time="1.55" steps="458"/></proof>
<proof prover="4"><result status="valid" time="1.65" steps="458"/></proof>
</goal>
<goal name="WP_parameter peek.18" expl="18. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter peek.19" expl="19. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.11"/></proof>
<proof prover="6"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="WP_parameter peek.20" expl="20. loop variant decrease">
<proof prover="0"><result status="valid" time="0.14" steps="104"/></proof>
......@@ -297,7 +297,7 @@
<goal name="WP_parameter poke_8bit.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.10" steps="103"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="3"><result status="valid" time="0.11"/></proof>
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter poke_8bit.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
......@@ -317,10 +317,10 @@
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter poke_8bit.9" expl="9. postcondition">
<proof prover="3"><result status="valid" time="2.02"/></proof>
<proof prover="3"><result status="valid" time="1.68"/></proof>
</goal>
<goal name="WP_parameter poke_8bit.10" expl="10. postcondition">
<proof prover="3"><result status="valid" time="1.26"/></proof>
<proof prover="3"><result status="valid" time="0.88"/></proof>
</goal>
</transf>
</goal>
......@@ -357,7 +357,7 @@
<goal name="WP_parameter poke_8bit_array.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.34" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="3"><result status="valid" time="1.40"/></proof>
<proof prover="3"><result status="valid" time="1.52"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter poke_8bit_array.7" expl="7. index in array bounds">
......@@ -446,7 +446,7 @@
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter poke.16" expl="16. precondition">
<proof prover="3"><result status="valid" time="0.86"/></proof>
<proof prover="3"><result status="valid" time="1.03"/></proof>
</goal>
<goal name="WP_parameter poke.17" expl="17. precondition">
<proof prover="3"><result status="valid" time="0.07"/></proof>
......@@ -508,14 +508,14 @@
<proof prover="0"><result status="valid" time="0.29" steps="129"/></proof>
</goal>
<goal name="WP_parameter poke.27" expl="27. loop invariant preservation">
<proof prover="0"><result status="valid" time="1.52" steps="125"/></proof>
<proof prover="0"><result status="valid" time="1.16" steps="125"/></proof>
</goal>
<goal name="WP_parameter poke.28" expl="28. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.75" steps="119"/></proof>
<proof prover="0"><result status="valid" time="0.49" steps="119"/></proof>
</goal>
<goal name="WP_parameter poke.29" expl="29. loop variant decrease">
<proof prover="0"><result status="valid" time="0.20" steps="104"/></proof>
<proof prover="3"><result status="valid" time="0.80"/></proof>
<proof prover="3"><result status="valid" time="0.86"/></proof>
</goal>
<goal name="WP_parameter poke.30" expl="30. type invariant">
<proof prover="0"><result status="valid" time="0.05" steps="88"/></proof>
......@@ -592,7 +592,7 @@
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter peekthenpoke.8" expl="8. assertion">
<proof prover="3"><result status="valid" time="0.71"/></proof>
<proof prover="3"><result status="valid" time="0.76"/></proof>
</goal>
<goal name="WP_parameter peekthenpoke.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
......@@ -646,7 +646,7 @@
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter pokethenpeek.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="1.07" steps="364"/></proof>
<proof prover="0"><result status="valid" time="1.26" steps="364"/></proof>
</goal>
<goal name="WP_parameter pokethenpeek.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.18" steps="97"/></proof>
......
......@@ -129,13 +129,11 @@
</goal>
<goal name="g8aa" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="5.02"/></proof>
<proof prover="4"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="g8bb" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="gtt">
<proof prover="0"><result status="valid" time="0.13" steps="80"/></proof>
......
This diff is collapsed.
......@@ -12,7 +12,7 @@
<goal name="WP_parameter min_elt" expl="VC for min_elt" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter min_elt.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.76" steps="183"/></proof>
<proof prover="0"><result status="valid" time="0.91" steps="183"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
......@@ -23,7 +23,7 @@
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter min_elt.3" expl="3. loop variant decrease">
<proof prover="0"><result status="valid" time="1.14" steps="296"/></proof>
<proof prover="0"><result status="valid" time="1.25" steps="296"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -88,7 +88,7 @@
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.16" steps="146"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="146"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.6" expl="6. postcondition">
......
......@@ -175,7 +175,7 @@
</goal>
<goal name="smoke1" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1" timelimit="15"><result status="unknown" time="0.59"/></proof>
<proof prover="1" timelimit="15"><result status="unknown" time="0.51"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......@@ -210,7 +210,7 @@
</goal>
<goal name="smoke6" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.98"/></proof>
<proof prover="1"><result status="unknown" time="0.83"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......@@ -309,7 +309,7 @@
</goal>
<goal name="f7" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.64"/></proof>
<proof prover="1"><result status="unknown" time="0.36"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="4.99"/></proof>
......@@ -329,7 +329,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Nth_Bv_bw_or" expanded="true">
<proof prover="0"><result status="valid" time="0.43" steps="190"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="190"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
......@@ -553,7 +553,7 @@
</goal>
<goal name="smoke1" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1" timelimit="15"><result status="unknown" time="0.75"/></proof>
<proof prover="1" timelimit="15"><result status="unknown" time="0.51"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......@@ -574,21 +574,21 @@
</goal>
<goal name="smoke4" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.68"/></proof>
<proof prover="1"><result status="unknown" time="0.49"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke5" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.67"/></proof>
<proof prover="1"><result status="unknown" time="0.49"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.03"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke6" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="1.25"/></proof>
<proof prover="1"><result status="unknown" time="0.87"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
<proof prover="4"><result status="timeout" time="4.99"/></proof>
......@@ -694,7 +694,7 @@
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="ok10" expanded="true">
<proof prover="0"><result status="valid" time="0.23" steps="112"/></proof>
<proof prover="0"><result status="valid" time="0.24" steps="112"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -917,7 +917,7 @@
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="ok10" expanded="true">
<proof prover="0"><result status="valid" time="0.23" steps="112"/></proof>
<proof prover="0"><result status="valid" time="0.25" steps="112"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -1006,7 +1006,7 @@
</goal>
<goal name="smoke2" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.65"/></proof>
<proof prover="1"><result status="unknown" time="0.43"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.97"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......@@ -1027,7 +1027,7 @@
</goal>
<goal name="smoke5" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.72"/></proof>
<proof prover="1"><result status="unknown" time="0.50"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
......
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