From 28f6ab6f3372ea42aabf7d20bc42c71d5548f25b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 14 Jun 2019 16:21:12 +0200
Subject: [PATCH] [WP] Prop name prettier in case of multiple call to the same
function
instead of caller_call_callee_requires_foo_2 we have
caller_call_callee_2_requires_foo .
---
.../wp/oracle_qualif/wp_call_pre.res.oracle | 2 +-
.../oracle_qualif/nupw-bcl-bts1120.res.oracle | 2 +-
.../oracle_qualif/dispatch_var.res.oracle | 2 +-
.../oracle_qualif/injector.0.res.oracle | 2 +-
.../oracle_qualif/user_collect.res.oracle | 6 ++--
src/plugins/wp/wpPropId.ml | 30 +++++++++++++++----
6 files changed, 32 insertions(+), 12 deletions(-)
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 9ff53cc2631..ac921a318be 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_2 : 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 0eb42debb65..2ba23416456 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_2 : 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 e3aa6c4c70f..98ab24cc12d 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_2 : 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 aabf5e4e8e0..03d5b7f2fd3 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_2 : 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 5e751c422ef..2a297e0ebef 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_2 : 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_2 : 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_2 : 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 b00f33bc3a3..894def5654e 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -368,6 +368,17 @@ struct
let get_ip ip =
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
| (PKTactic | PKCheck | PKProp | PKPropLoop) , p -> get_ip p
@@ -377,11 +388,20 @@ 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_basename p =
let basename = get_prop_id_base p in
--
GitLab