Commit 39ac5765 authored by MARCHE Claude's avatar MARCHE Claude

details

parent a10fd6b7
......@@ -155,19 +155,24 @@ Release Notes (details in file CHANGES):
== TODO ==
* Document src/core/trans.mli, and fill the paragraph on
transformations in the tutorial: doc/api.tex, section 4.7 "Applying
transformations"
* fix bug 18953 : (<>) not allowed as prefix form
* finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
* integrate server feature done by Johannes
* Coq realization of bitvector theory
* DONE Coq realization of bitvector theory
* make counter-examples feature more robust
* support for both isabelle 2014 and 2015
* DONE support for both isabelle 2014 and 2015
+ bugfix for installation
* review support for division operators by SMT provers
* DONE review support for division operators by SMT provers
* take some time to fix some bugs of the BTS: 18029 at least
......@@ -176,7 +181,7 @@ Release Notes (details in file CHANGES):
alt-ergo -replay <file>.agr
* make the strategy feature public and documented. Possibly generate
default stratregies dynamically at the time of why3 config --detect,
default strategies dynamically at the time of why3 config --detect,
using the provers detected : for that, we can annotated the provers in
prover-detection-data.conf to tell if they should be used in the strategies,
with which priority
......@@ -187,7 +192,7 @@ Release Notes (details in file CHANGES):
. or, on the contrary, favor splitting
. or, favor timelimt increase...
. or, favor timelimit increase...
......
......@@ -5,105 +5,105 @@
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.1" timelimit="10" memlimit="1000"/>
<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="3" name="Alt-Ergo" version="0.95.2" timelimit="10" 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">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="10"><result status="valid" time="0.17" steps="55"/></proof>
<proof prover="3"><result status="valid" time="0.17" steps="55"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchAnyMidPoint" sum="cf35a6556f511e3fa459bea0349c2cf8" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="10"><result status="valid" time="0.02" steps="39"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="39"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="0bac534b34ae6ec72cbe896cc4f66587" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search">
<transf name="split_goal_wp">
<theory name="BinarySearchInt32" sum="b978ced2b74f7ab893e5b3a8d23ebe1f" 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="71"/></proof>
<proof prover="5"><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="73"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="75"/></proof>
</goal>
<goal name="WP_parameter binary_search.3" expl="3. integer overflow">
<proof prover="3"><result status="valid" time="0.12" steps="90"/></proof>
<proof prover="5"><result status="valid" time="0.12" steps="94"/></proof>
</goal>
<goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="76"/></proof>
<proof prover="5"><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="79"/></proof>
<proof prover="5"><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="81"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
<goal name="WP_parameter binary_search.7" expl="7. integer overflow">
<proof prover="3"><result status="valid" time="0.02" steps="87"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="91"/></proof>
</goal>
<goal name="WP_parameter binary_search.8" expl="8. division by zero">
<proof prover="3"><result status="valid" time="0.01" steps="84"/></proof>
<proof prover="5"><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="100"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.10" expl="10. integer overflow">
<proof prover="3"><result status="valid" time="0.52" steps="116"/></proof>
<proof prover="5"><result status="valid" time="0.24" steps="116"/></proof>
</goal>
<goal name="WP_parameter binary_search.11" expl="11. assertion">
<proof prover="3"><result status="valid" time="1.48" steps="136"/></proof>
<proof prover="5"><result status="valid" time="0.54" 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="91"/></proof>
<proof prover="5"><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="95"/></proof>
<proof prover="5"><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="112"/></proof>
<proof prover="5"><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="99"/></proof>
<proof prover="5"><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="5"><result status="valid" time="1.33" steps="180"/></proof>
<proof prover="5"><result status="valid" time="2.58" 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="99"/></proof>
<proof prover="5"><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="95"/></proof>
<proof prover="5"><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="97"/></proof>
<proof prover="5"><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="101"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="113"/></proof>
</goal>
<goal name="WP_parameter binary_search.21" expl="21. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02" steps="101"/></proof>
<proof prover="5"><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="5"><result status="valid" time="1.27" steps="181"/></proof>
<proof prover="5"><result status="valid" time="2.43" steps="181"/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="3"><result status="valid" time="0.02" steps="101"/></proof>
<proof prover="5"><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="128"/></proof>
<proof prover="5"><result status="valid" time="0.08" steps="125"/></proof>
</goal>
<goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition">
<proof prover="3"><result status="valid" time="0.01" steps="90"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="90"/></proof>
</goal>
</transf>
</goal>
......
......@@ -126,17 +126,17 @@ let simpl_divmod _ls t1 t2 _ty =
let simpl_minmax _ls v1 v2 _ty =
match v1,v2 with
| Term t1, Term t2 ->
if t_equal t1 t2 then v1 else
if t_equal t1 t2 then v1 else
raise Undetermined
(*
t_app_value ls [v1;v2] ty
*)
| _ ->
| _ ->
raise Undetermined
(*
t_app_value ls [v1;v2] ty
*)
let eval_int_rel op _ls l _ty =
match l with
| [t1 ; t2] ->
......@@ -162,7 +162,7 @@ let eval_int_uop op _ls l _ty =
raise Undetermined
(* t_app_value ls l ty *)
end
| _ -> assert false
| _ -> assert false
let built_in_theories =
......@@ -584,7 +584,7 @@ and reduce_app engine st ls ~orig ty rem_cont =
else
if ls_equal ls fs_func_app then
match st with
| t2 :: t1 :: rem_st ->
| t2 :: t1 :: rem_st ->
begin
try
reduce_func_app ~orig ty rem_st t1 t2 rem_cont
......@@ -981,6 +981,9 @@ let extract_rule _km t =
| Decl.Dparam _ | Decl.Dind _ -> ()
in
*)
(* TODO : verifier que les variables de droite, aussi bien term que type,
apparaissent a gauche *)
let rec aux acc t =
match t.t_node with
| Tquant(Tforall,q) ->
......
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