From 3cf336682380cdf4d4bc6685a1e745707c3ee00b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 14 Jun 2019 15:29:58 +0200
Subject: [PATCH] [WP] make sure that the prop_id names are unique
---
.../wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle | 2 +-
.../wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle | 2 +-
.../wp_hoare/oracle_qualif/dispatch_var.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/injector.0.res.oracle | 2 +-
.../wp_typed/oracle_qualif/user_collect.res.oracle | 6 +++---
src/plugins/wp/wpPropId.ml | 10 +++++++++-
6 files changed, 16 insertions(+), 8 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 fee194ce70a..9ff53cc2631 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_requires_qed_ok_Rf_2 : 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 ac5a5264006..0eb42debb65 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_requires_ok_2 : 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 e18208021cc..e3aa6c4c70f 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_requires_2 : 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 5bfd4b969d1..aabf5e4e8e0 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_requires_2 : 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 8676944fb53..5e751c422ef 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_requires_2 : 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_requires_2 : 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_requires_2 : 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 da6d8ed1239..b00f33bc3a3 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -383,7 +383,7 @@ struct
(Kernel_function.find_englobing_kf stmt)
in Printf.sprintf "%s_call_%s" kf_name_of_stmt (get_ip pre)
- 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
@@ -393,6 +393,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
(* -------------------------------------------------------------------------- *)
--
GitLab