Commit a5c19e79 authored by MARCHE Claude's avatar MARCHE Claude

finally remove checksums from why3session.xml

parent f50e6f8d
......@@ -2,51 +2,51 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Z3" version="3.2" timelimit="10" memlimit="0"/>
<prover id="3" name="veriT" version="201310" timelimit="5" memlimit="4000"/>
<file name="../mccarthy.mlw" expanded="true">
<theory name="McCarthy91" expanded="true">
<goal name="WP_parameter f91" expl="VC for f91" sum="b4bc2875eac8410bbf400db454127714" expanded="true">
<proof prover="0" timelimit="2"><result status="valid" time="0.00"/></proof>
<proof prover="1" timelimit="2"><result status="valid" time="0.02"/></proof>
<theory name="McCarthy91" sum="07974fb6f44e79c82bfe8056427fd06c" expanded="true">
<goal name="WP_parameter f91" expl="VC for f91" expanded="true">
<proof prover="0" timelimit="2"><result status="valid" time="0.02"/></proof>
<proof prover="1" timelimit="2"><result status="valid" time="0.00"/></proof>
<proof prover="2" timelimit="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec" expl="VC for f91_nonrec" sum="1ed4d62bb25f1a93fab7830968d41d88" expanded="true">
<goal name="WP_parameter f91_nonrec" expl="VC for f91_nonrec" expanded="true">
<transf name="split_goal" expanded="true">
<goal name="WP_parameter f91_nonrec.1" expl="1. loop invariant init" sum="99821fdb8842a91d7deda4441eff2ebd" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter f91_nonrec.1" expl="1. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.2" expl="2. loop invariant preservation" sum="06ec26f24367110577f61e032ba308d5" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<goal name="WP_parameter f91_nonrec.2" expl="2. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.3" expl="3. loop variant decrease" sum="4cc16d766f9bfea8c706a712473543d4" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter f91_nonrec.3" expl="3. loop variant decrease" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.4" expl="4. loop invariant preservation" sum="c9dd0f925268cbda69c1fec728f402a5" expanded="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.24"/></proof>
<goal name="WP_parameter f91_nonrec.4" expl="4. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.39"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.5" expl="5. loop variant decrease" sum="aaa1005c01f190e89d8dd5eb47c5b43a" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter f91_nonrec.5" expl="5. loop variant decrease" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.6" expl="6. postcondition" sum="161d3b4554721e0b60bca0b5a845b922" expanded="true">
<goal name="WP_parameter f91_nonrec.6" expl="6. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
......
......@@ -598,10 +598,12 @@ let rec save_goal ctxt fmt g =
let shape = Tc.string_of_shape g.goal_shape in
assert (shape <> "");
fprintf fmt
"@\n@[<v 0>@[<h><goal@ %a%a%a%a>@]"
"@\n@[<v 0>@[<h><goal@ %a%a%a>@]"
save_ident g.goal_name
(opt_string "expl") g.goal_expl
(* no more checksum in why3session.xml
(opt save_checksum "sum") g.goal_checksum
*)
(save_bool_def "expanded" false) g.goal_expanded;
let sum =
match g.goal_checksum with
......@@ -1498,7 +1500,7 @@ let read_sum_and_shape ch =
with
| End_of_file ->
raise (ShapesFileError "shapes files corrupted (premature end of file), ignored");
| Exit -> sum, Buffer.contents shape
| Exit -> String.copy sum, Buffer.contents shape
let use_shapes = ref true
......@@ -2024,7 +2026,7 @@ end = struct
let use_shapes = ref true
let set_use_shapes b = use_shapes := b
let associate ~theory_was_fully_up_to_date
let associate ~theory_was_fully_up_to_date
(from_goals: 'ffrom goal list) (to_goals: 'tto goal list) :
('tto goal * ('ffrom goal * bool) option) list =
let from_goals : ffrom goal list =
......@@ -2032,9 +2034,9 @@ end = struct
let to_goals : tto goal list =
Obj.magic (to_goals : 'tto goal list) in
let associated : (tto goal * (ffrom goal * bool) option) list =
AssoGoals.associate
AssoGoals.associate
~theory_was_fully_up_to_date
~use_shapes:!use_shapes from_goals to_goals
~use_shapes:!use_shapes from_goals to_goals
in
(Obj.magic associated : ('tto goal * ('ffrom goal * bool) option) list)
......@@ -2302,7 +2304,7 @@ and merge_trans ~ctxt ~theories env to_goal _ from_transf =
let associated =
Debug.dprintf debug "[Info] associate_subgoals, shape_version = %d@\n"
env.session.session_shape_version;
AssoGoals.associate
AssoGoals.associate
~theory_was_fully_up_to_date:ctxt.theory_is_fully_up_to_date
from_transf.transf_goals to_transf.transf_goals
in
......@@ -2364,11 +2366,19 @@ let merge_theory ~ctxt ~theories env from_th to_th =
| Some s1, Some s2 -> Tc.equal_checksum s1 s2
}
in
Debug.dprintf debug
"[Theory checksum] fully up to date = %b@."
ctxt.theory_is_fully_up_to_date;
List.iter
(fun to_goal ->
try
let from_goal =
Mstr.find to_goal.goal_name.Ident.id_string from_goals in
Debug.dprintf debug
"[Goal checksum] goal %s: old sum = %a, new sum = %a@."
to_goal.goal_name.Ident.id_string
(Pp.print_option Tc.print_checksum) from_goal.goal_checksum
(Pp.print_option Tc.print_checksum) to_goal.goal_checksum;
let goal_obsolete =
match to_goal.goal_checksum, from_goal.goal_checksum with
| None, _ -> assert false
......@@ -2607,7 +2617,7 @@ and add_transf_to_goal ~keygen env to_goal from_transf =
let associated =
Debug.dprintf debug "[Info] associate_subgoals, shape_version = %d@\n"
env.session.session_shape_version;
AssoGoals.associate
AssoGoals.associate
~theory_was_fully_up_to_date:false
from_transf.transf_goals to_transf.transf_goals in
List.iter (function
......
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