Skip to content

GitLab

why3
why3
Commit fb9ff35a authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

fix #17181

parent e26922de
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 718 additions and 652 deletions
examples/avl/priority_queue/why3session.xml
View file @ fb9ff35a
This diff is collapsed.
examples/avl/ral/why3session.xml
View file @ fb9ff35a
......@@ -4,28 +4,28 @@
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../ral.mlw">
<theory name="RAL" sum="b85ea65c6b3b2e84fb0a259ea33ee2c5">
<goal name="assoc">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<file name="../ral.mlw" expanded="true">
<theory name="RAL" sum="b85ea65c6b3b2e84fb0a259ea33ee2c5" expanded="true">
<goal name="M.assoc">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="neutral">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="M.neutral">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="assoc">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="M.M.assoc">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="neutral">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="M.M.neutral">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter zero" expl="VC for zero">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="M.WP_parameter zero" expl="VC for zero">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter op" expl="VC for op">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="M.WP_parameter op" expl="VC for op">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter measure" expl="VC for measure">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="D.WP_parameter measure" expl="VC for measure">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sum_measure_is_length" expl="VC for sum_measure_is_length">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -33,35 +33,35 @@
<goal name="WP_parameter selected_part" expl="VC for selected_part">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="assoc">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="Sel.M.assoc">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="neutral">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="Sel.M.neutral">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="sum_def_nil">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="Sel.M.sum_def_nil">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="sum_def_cons">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="Sel.M.sum_def_cons">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="balancing_positive">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="Sel.balancing_positive">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="selection_empty">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<goal name="Sel.selection_empty">
<proof prover="1" timelimit="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter avl AVL M zero" expl="VC for avl AVL M zero">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="Sel.WP_parameter avl AVL M zero" expl="VC for avl AVL M zero">
<proof prover="1" timelimit="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter avl AVL M op" expl="VC for avl AVL M op">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="Sel.WP_parameter avl AVL M op" expl="VC for avl AVL M op">
<proof prover="1" timelimit="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter avl AVL D measure" expl="VC for avl AVL D measure">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="Sel.WP_parameter avl AVL D measure" expl="VC for avl AVL D measure">
<proof prover="1" timelimit="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter avl AVL selected_part" expl="VC for avl AVL selected_part">
<proof prover="1"><result status="valid" time="0.30"/></proof>
<goal name="Sel.WP_parameter avl AVL selected_part" expl="VC for avl AVL selected_part">
<proof prover="1" timelimit="3"><result status="valid" time="0.57"/></proof>
</goal>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......
examples/avl/tables/why3session.xml
View file @ fb9ff35a
This diff is collapsed.
examples/bts/17181.mlw 0 → 100644
View file @ fb9ff35a
theory T
namespace A
goal g:true
end
namespace B
goal g:false
end
end
module A
predicate p
predicate q
namespace B
let f () : unit ensures { p } = ()
end
namespace C
let f () : unit ensures { q <-> p } = ()
end
end
examples/bts/17181/why3session.xml 0 → 100644
View file @ fb9ff35a
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="3" memlimit="1000"/>
<file name="../17181.mlw" expanded="true">
<theory name="T" sum="bf985426bbce7996e2481c8e25f14156" expanded="true">
<goal name="A.g" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="B.g" expanded="true">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
</theory>
<theory name="A" sum="2bae57918a7b687b2d8d2a31ec13cb69" expanded="true">
<goal name="B.WP_parameter f" expl="VC for f" expanded="true">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="C.WP_parameter f" expl="VC for f" expanded="true">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
</theory>
</file>
</why3session>
src/session/session.ml
View file @ fb9ff35a
......@@ -491,7 +491,13 @@ exception NoTask
let goal_task g = Opt.get_exn NoTask g.goal_task
let goal_task_option g = g.goal_task
let goal_expl g = Opt.get_def g.goal_name.Ident.id_string g.goal_expl
let goal_expl g =
match g.goal_expl with
| Some s -> s
| None ->
try let _,_,l = restore_path g.goal_name in
String.concat "." l
with Not_found -> g.goal_name.Ident.id_string
(************************)
(* saving state on disk *)
......@@ -564,25 +570,14 @@ let save_proof_attempt fmt ((id,tl,ml),a) =
fprintf fmt "</proof>@]"
let save_ident fmt id =
fprintf fmt "name=\"%a\"" save_string id.Ident.id_string;
(* location info is useless, and takes a lot of place *)
(*
match id.Ident.id_loc with
| None -> ()
| Some loc ->
let file,lnum,cnumb,cnume = Loc.get loc in
let file = Sysutil.relativize_filename !session_dir_for_save file in
fprintf fmt
"@ locfile=\"%a\"@ loclnum=\"%i\" loccnumb=\"%i\" loccnume=\"%i\""
save_string file lnum cnumb cnume
*)
()
(*
let save_label fmt s =
fprintf fmt "@\n@[<hov 1><label@ name=\"%a\"/>@]" save_string s.Ident.lab_string
*)
let n=
try
let (_,_,l) = Theory.restore_path id in
String.concat "." l
with Not_found -> id.Ident.id_string
in
fprintf fmt "name=\"%a\"" save_string n
module Compr = Compress.Compress_z
type save_ctxt = {
......@@ -2364,8 +2359,13 @@ let merge_theory ~ctxt ~theories env from_th to_th =
List.iter
(fun to_goal ->
try
let from_goal =
Mstr.find to_goal.goal_name.Ident.id_string from_goals in
let to_goal_name =
try
let (_,_,l) = restore_path to_goal.goal_name
in String.concat "." l
with Not_found -> to_goal.goal_name.Ident.id_string
in
let from_goal = Mstr.find to_goal_name from_goals in
Debug.dprintf debug
"[Goal checksum] goal %s: old sum = %a, new sum = %a@."
to_goal.goal_name.Ident.id_string
......
src/whyml/mlw_wp.ml
View file @ fb9ff35a
......@@ -946,7 +946,13 @@ let rec unabsurd f = match f.t_node with
let add_wp_decl km name f uc =
(* prepare a proposition symbol *)
let s = "WP_parameter " ^ name.id_string in
let lab = Ident.create_label ("expl:VC for " ^ name.id_string) in
(* set a proper explanation *)
let n =
try let _,_,l = restore_path name in
String.concat "." l
with Not_found -> name.id_string
in
let lab = Ident.create_label ("expl:VC for " ^ n) in
let label = Slab.add lab name.id_label in
let id = id_fresh ~label ?loc:name.id_loc s in
let pr = create_prsymbol id in
......
tests/test_compute.why
View file @ fb9ff35a
theory A
predicate p
predicate q
goal G1 : p /\ q
goal G2 : p -> q
goal G3 : p && q
end
theory Test
goal g1: true
......
tests/test_compute/why3session.xml
View file @ fb9ff35a
This diff is collapsed.
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