Commit e3a14168 authored by MARCHE Claude's avatar MARCHE Claude

Fix warning and upgrade an Alt-Ergo proof

parent e8ecc8d2
......@@ -7,6 +7,7 @@
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.3" timelimit="10" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../binary_search.mlw" expanded="true">
<theory name="BinarySearch" sum="6edf021e1310395e54f253f514978225" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
......@@ -22,87 +23,87 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="2089995b9d71a591dc8d378af11dce53" expanded="true">
<theory name="BinarySearchInt32" sum="0bac534b34ae6ec72cbe896cc4f66587" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search.1" expl="1. integer overflow">
<proof prover="3"><result status="valid" time="0.02" steps="70"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="WP_parameter binary_search.2" expl="2. integer overflow">
<proof prover="3"><result status="valid" time="0.01" steps="72"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="73"/></proof>
</goal>
<goal name="WP_parameter binary_search.3" expl="3. integer overflow">
<proof prover="3"><result status="valid" time="0.12" steps="88"/></proof>
<proof prover="3"><result status="valid" time="0.12" steps="90"/></proof>
</goal>
<goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="75"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="76"/></proof>
</goal>
<goal name="WP_parameter binary_search.5" expl="5. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="78"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="79"/></proof>
</goal>
<goal name="WP_parameter binary_search.6" expl="6. integer overflow">
<proof prover="3"><result status="valid" time="0.02" steps="80"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="81"/></proof>
</goal>
<goal name="WP_parameter binary_search.7" expl="7. integer overflow">
<proof prover="3"><result status="valid" time="0.02" steps="86"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
<goal name="WP_parameter binary_search.8" expl="8. division by zero">
<proof prover="3"><result status="valid" time="0.01" steps="83"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="84"/></proof>
</goal>
<goal name="WP_parameter binary_search.9" expl="9. integer overflow">
<proof prover="3"><result status="valid" time="0.04" steps="99"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="100"/></proof>
</goal>
<goal name="WP_parameter binary_search.10" expl="10. integer overflow">
<proof prover="3"><result status="valid" time="0.52" steps="114"/></proof>
<proof prover="3"><result status="valid" time="0.52" steps="116"/></proof>
</goal>
<goal name="WP_parameter binary_search.11" expl="11. assertion">
<proof prover="3"><result status="valid" time="1.48" steps="133"/></proof>
<proof prover="3"><result status="valid" time="1.48" steps="136"/></proof>
</goal>
<goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
<proof prover="3"><result status="valid" time="0.01" steps="90"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="91"/></proof>
</goal>
<goal name="WP_parameter binary_search.13" expl="13. integer overflow">
<proof prover="3"><result status="valid" time="0.01" steps="94"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="95"/></proof>
</goal>
<goal name="WP_parameter binary_search.14" expl="14. integer overflow">
<proof prover="3"><result status="valid" time="0.03" steps="111"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="112"/></proof>
</goal>
<goal name="WP_parameter binary_search.15" expl="15. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02" steps="98"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="8.76" steps="176"/></proof>
<proof prover="5"><result status="valid" time="1.33" steps="180"/></proof>
</goal>
<goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
<proof prover="3"><result status="valid" time="0.02" steps="98"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.18" expl="18. index in array bounds">
<proof prover="3"><result status="valid" time="0.01" steps="94"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="95"/></proof>
</goal>
<goal name="WP_parameter binary_search.19" expl="19. integer overflow">
<proof prover="3"><result status="valid" time="0.01" steps="96"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="97"/></proof>
</goal>
<goal name="WP_parameter binary_search.20" expl="20. integer overflow">
<proof prover="3"><result status="valid" time="0.02" steps="100"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="101"/></proof>
</goal>
<goal name="WP_parameter binary_search.21" expl="21. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02" steps="100"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="101"/></proof>
</goal>
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="60"><result status="valid" time="14.15" steps="177"/></proof>
<proof prover="3" timelimit="60"><undone/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="3"><result status="valid" time="0.02" steps="100"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="101"/></proof>
</goal>
<goal name="WP_parameter binary_search.24" expl="24. postcondition">
<proof prover="3"><result status="valid" time="2.32" steps="126"/></proof>
<proof prover="3"><result status="valid" time="2.32" steps="128"/></proof>
</goal>
<goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition">
<proof prover="3"><result status="valid" time="0.01" steps="89"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="90"/></proof>
</goal>
</transf>
</goal>
......
......@@ -6,7 +6,7 @@ module M
type t = A | B
type s = { field1 : t -> t ; field2 : t -> t }
function const (x:'b) : 'a -> 'b = \y:'a.x
function const (x:'b) : 'a -> 'b = \_:'a.x
predicate p (u:s) (a b:t) = u.field1 = const a /\ u.field2 = const b
......
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