diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index fee194ce70ab07b10bf6bdf595543c7b59b09f82..ac921a318be08275381f558f6f55e0a47a049d54 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -13,7 +13,7 @@
[wp] [Qed] Goal typed_call_main_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_call_main_call_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
-[wp] [Alt-Ergo] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
+[wp] [Alt-Ergo] Goal typed_double_call_call_f_2_requires_qed_ok_Rf : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_main_ensures_qed_ok_Emain : Valid
[wp] [Qed] Goal typed_main_call_f_requires_qed_ok_Rf : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
index ac5a52640069fe4f37d2173e5c5c77778a44fa53..2ba23416456faa39cde87569f6ab9693ef9bc593 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
@@ -17,7 +17,7 @@
[wp] [Qed] Goal typed_g_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_g_assigns_normal_part3 : Valid
[wp] [Qed] Goal typed_unreachable_smt_with_contract_ensures_ok_2 : Valid
-[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_requires_ok : Valid
+[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_2_requires_ok : Valid
[wp] Proved goals: 8 / 8
Qed: 8
[wp] Report in: 'tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.0.report.json'
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
index e18208021ccb21482035e39a7353f2c3dcf98688..98ab24cc12de61c5d5ae89cbc5e7f47c915dc1c0 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
@@ -65,7 +65,7 @@
[wp] [Qed] Goal typed_ref_call_ref_valid_assigns_normal_part4 : Valid
[wp] [Qed] Goal typed_ref_call_ref_valid_assigns_normal_part5 : Valid
[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_requires : Valid
-[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_requires : Valid
+[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_2_requires : Valid
[wp] [Qed] Goal typed_ref_call_two_ref_ensures : Valid
[wp] [Qed] Goal typed_ref_call_two_ref_assigns_exit_part1 : Valid
[wp] [Qed] Goal typed_ref_call_two_ref_assigns_exit_part2 : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
index 5bfd4b969d1181a464dfba7b4c2af80db87bcd2d..03d5b7f2fd3a7dcd17af11e41b87908e51636da0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
@@ -5,7 +5,7 @@
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
[wp] [Qed] Goal typed_f_call_g_requires : Valid
-[wp] [Qed] Goal typed_f_call_g_requires : Valid
+[wp] [Qed] Goal typed_f_call_g_2_requires : Valid
[wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok_2 : Valid
[wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok_3 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
index 8676944fb53b5219663b759b05710eb35ea5ee66..2a297e0ebefb2b37d8791372db2d79f4f853723e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
@@ -8,19 +8,19 @@
[wp] [Alt-Ergo] Goal typed_caller_ensures_P1 : Valid
[wp] [Alt-Ergo] Goal typed_caller_ensures_P2 : Valid
[wp] [Alt-Ergo] Goal typed_caller_call_job_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller_call_job_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller_call_job_2_requires : Valid
[wp] [Qed] Goal typed_caller2_ensures_K : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_Q1 : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_Q2 : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_R : Valid
[wp] [Alt-Ergo] Goal typed_caller2_call_job2_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller2_call_job2_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller2_call_job2_2_requires : Valid
[wp] [Qed] Goal typed_caller3_ensures_K : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_Q1 : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_Q2 : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_R : Valid
[wp] [Alt-Ergo] Goal typed_caller3_call_job3_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller3_call_job3_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller3_call_job3_2_requires : Valid
[wp] [Qed] Goal typed_job_ensures_K : Valid
[wp] [Qed] Goal typed_job_ensures_P : Valid
[wp] [Qed] Goal typed_job_assigns_part1 : Valid
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 2cde75506a5960e32eb8a2e6493738a24241bedb..894def5654e6c88349bb8a1f22669a3cf852d950 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -232,22 +232,27 @@ module PropId =
(* --- Lagacy Naming --- *)
(* -------------------------------------------------------------------------- *)
-module LegacyNames :
+module NameUniquify(D:Datatype.S_with_collections)(S:sig
+ val name: string
+ val basename: D.t -> string
+ end) :
sig
- val get_prop_id_name: prop_id -> string
-end = struct
+ val unique_basename: D.t -> string
+end
+=
+struct
module NamesTbl = State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
(struct
- let name = "WpPropertyNames"
+ let name = S.name^"Names"
let dependencies = [ ]
let size = 97
end)
module IndexTbl =
- State_builder.Hashtbl(PropId.Hashtbl)(Datatype.String)
+ State_builder.Hashtbl(D.Hashtbl)(Datatype.String)
(struct
- let name = "WpPropertyIndex"
+ let name = S.name^"Index"
let dependencies =
[ Ast.self;
NamesTbl.self;
@@ -258,6 +263,38 @@ end = struct
let size = 97
end)
+
+ (** returns the name that should be returned by the function [get_prop_name_id]
+ if the given property has [name] as basename. That name is reserved so that
+ [get_prop_name_id prop] can never return an identical name. *)
+ let reserve_name_id pid =
+ let basename = S.basename pid in
+ try
+ let speed_up_start = NamesTbl.find basename in
+ (* this basename is already reserved *)
+ let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
+ in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
+ unique_name
+ with Not_found -> (* first time that basename is reserved *)
+ NamesTbl.add basename 2 ;
+ basename
+
+ (** returns a unique name identifying the property.
+ This name is built from the basename of the property. *)
+ let unique_basename pid =
+ try IndexTbl.find pid
+ with Not_found -> (* first time we are asking for a name for that [ip] *)
+ let unique_name = reserve_name_id pid in
+ IndexTbl.add pid unique_name ;
+ unique_name
+
+end
+
+module LegacyNames :
+sig
+ val get_prop_id_name: prop_id -> string
+end = struct
+
let base_id_prop_txt = Property.LegacyNames.get_prop_name_id
let basename_of_prop_id p =
@@ -296,29 +333,17 @@ end = struct
Printf.sprintf "%s_part%06d" basename (succ k)
in normalize_basename basename
- (** returns the name that should be returned by the function [get_prop_name_id]
- if the given property has [name] as basename. That name is reserved so that
- [get_prop_name_id prop] can never return an identical name. *)
- let reserve_name_id pid =
- let basename = get_prop_id_basename pid in
- try
- let speed_up_start = NamesTbl.find basename in
- (* this basename is already reserved *)
- let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
- in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
- unique_name
- with Not_found -> (* first time that basename is reserved *)
- NamesTbl.add basename 2 ;
- basename
+
+ module UniquifyPropId = NameUniquify(PropId)(struct
+ let name = "WpProperty"
+ let basename = get_prop_id_basename
+ end)
+
(** returns a unique name identifying the property.
This name is built from the basename of the property. *)
let get_prop_id_name pid =
- try IndexTbl.find pid
- with Not_found -> (* first time we are asking for a name for that [ip] *)
- let unique_name = reserve_name_id pid in
- IndexTbl.add pid unique_name ;
- unique_name
+ UniquifyPropId.unique_basename pid
end
@@ -332,45 +357,27 @@ sig
end =
struct
- module NamesTbl = State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
- (struct
- let name = "Wp.WpPropId.Names.NamesTbl"
- let dependencies = [ ]
- let size = 97
- end)
-
- module IndexTbl =
- State_builder.Hashtbl(Property.Hashtbl)(Datatype.String)
- (struct
- let name = "Wp.WpPropId.Names.IndexTbl"
- let dependencies =
- [ Ast.self;
- NamesTbl.self;
- Globals.Functions.self;
- Annotations.code_annot_state;
- Annotations.funspec_state;
- Annotations.global_state ]
- let size = 97
- end)
-
- let compute_ip ip =
- let truncate = max 20 (Wp_parameters.TruncPropIdFileName.get ()) in
- let basename = Property.Names.get_prop_basename ~truncate ip in
- try
- let speed_up_start = NamesTbl.find basename in
- let n,unique_name = Extlib.make_unique_name
- NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
- in NamesTbl.replace basename (succ n) ;
- unique_name
- with Not_found -> (* first time that basename is reserved *)
- NamesTbl.add basename 2 ; basename
+ (** Uniquify the first part of the prop_id *)
+ module Uniquify1 = NameUniquify(Property)(struct
+ let name = "Wp.WpPropId.Names."
+ let basename ip =
+ let truncate = max 20 (Wp_parameters.TruncPropIdFileName.get ()) in
+ Property.Names.get_prop_basename ~truncate ip
+ end)
let get_ip ip =
- try IndexTbl.find ip
- with Not_found -> (* first time we are asking for a name for that [ip] *)
- let unique_name = compute_ip ip in
- IndexTbl.add ip unique_name ;
- unique_name
+ Uniquify1.unique_basename ip
+
+ (** Uniquify call-site for precondition check. So
+ that precondition of the same call-site are grouped *)
+ module CallSite = Datatype.Triple_with_collections
+ (Kernel_function)(Kernel_function)(Stmt)
+ (struct let module_name = "Wp.WpPropId.CallSite" end)
+ module Uniquify_Stmt = NameUniquify(CallSite)(struct
+ let name = "Wp.WpPropId.Names3."
+ let basename (caller_kf,callee_kf,_stmt) =
+ (Kernel_function.get_name caller_kf)^"_call_"^(Kernel_function.get_name callee_kf)
+ end)
let get_prop_id_base p =
match p.p_kind , p.p_prop with
@@ -381,13 +388,22 @@ struct
| PKVarPos , p -> get_ip p ^ "_positive"
| PKAFctOut , p -> get_ip p ^ "_normal"
| PKAFctExit , p -> get_ip p ^ "_exit"
- | PKPre(_kf,stmt,pre) , _ ->
- let kf_name_of_stmt =
- Kernel_function.get_name
- (Kernel_function.find_englobing_kf stmt)
- in Printf.sprintf "%s_call_%s" kf_name_of_stmt (get_ip pre)
+ | PKPre(callee_kf,stmt,pre) , _ ->
+ let caller_kf = Kernel_function.find_englobing_kf stmt in
+ let call_string =
+ Uniquify_Stmt.unique_basename (caller_kf,callee_kf,stmt)
+ in
+ (** remove name of callee kernel function given by get_ip *)
+ let ip_string = get_ip pre in
+ let ip_string =
+ Extlib.opt_conv ip_string
+ (Extlib.string_del_prefix
+ ((Kernel_function.get_name callee_kf)^"_")
+ ip_string)
+ in
+ call_string^"_"^ip_string
- let get_prop_id_name p =
+ let get_prop_id_basename p =
let basename = get_prop_id_base p in
match p.p_part with
| None -> basename
@@ -397,6 +413,14 @@ struct
if n < 1000 then Printf.sprintf "%s_part%03d" basename (succ k) else
Printf.sprintf "%s_part%06d" basename (succ k)
+ module Uniquify2 = NameUniquify(PropId)(struct
+ let name = "Wp.WpPropId.Names2."
+ let basename = get_prop_id_basename
+ end)
+
+ let get_prop_id_name p =
+ Uniquify2.unique_basename p
+
end
(* -------------------------------------------------------------------------- *)