From 6333b7206269ffc479a2441191dbc36a604cd721 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 10 Feb 2021 16:00:28 +0100
Subject: [PATCH] [wp] suppress useless code
---
src/plugins/wp/cfgAnnot.ml | 2 +-
src/plugins/wp/normAtLabels.ml | 7 +------
src/plugins/wp/normAtLabels.mli | 3 +--
src/plugins/wp/wpStrategy.ml | 2 +-
4 files changed, 4 insertions(+), 10 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index f14ac822df1..8de5afd5be0 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -295,7 +295,7 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
type data = code_assertions
let name = "Wp.CfgAnnot.CodeAssertions"
let compile (kf,stmt) =
- let labels = NormAtLabels.labels_assert_before ~kf stmt in
+ let labels = NormAtLabels.labels_assert ~kf stmt in
let normalize_pred p = NormAtLabels.preproc_annot labels p in
reverse_code_assertions @@
Annotations.fold_code_annot
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index 7a52640077e..0f6ebe895ab 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -181,15 +181,10 @@ let labels_stmt_assigns_l ~kf s l_post = function
(* --- User Assertions in Functions Code --- *)
(* -------------------------------------------------------------------------- *)
-let labels_assert_before ~kf s = function
+let labels_assert ~kf s = function
| BuiltinLabel Here -> Clabels.stmt s
| l -> labels_fct ~kf ~at:s l
-let labels_assert_after ~kf s l_post = function
- | BuiltinLabel Old -> Clabels.stmt s
- | BuiltinLabel Here as l -> option l l_post
- | l -> labels_fct ~kf ~at:s l
-
let labels_loop s = function
(* In invariant preservation/establishment, LoopCurrent is Here. *)
| BuiltinLabel (Here | LoopCurrent) -> Clabels.here
diff --git a/src/plugins/wp/normAtLabels.mli b/src/plugins/wp/normAtLabels.mli
index 2becd6c715a..affd569c595 100644
--- a/src/plugins/wp/normAtLabels.mli
+++ b/src/plugins/wp/normAtLabels.mli
@@ -32,8 +32,7 @@ val labels_empty : label_mapping
val labels_fct_pre : label_mapping
val labels_fct_post : label_mapping
val labels_fct_assigns : label_mapping
-val labels_assert_before : kf:kernel_function -> stmt -> label_mapping
-val labels_assert_after : kf:kernel_function -> stmt -> c_label option -> label_mapping
+val labels_assert : kf:kernel_function -> stmt -> label_mapping
val labels_loop : stmt -> label_mapping
val labels_stmt_pre : kf:kernel_function -> stmt -> label_mapping
val labels_stmt_post : kf:kernel_function -> stmt -> label_mapping
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index 420016431a7..1166868e973 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -268,7 +268,7 @@ let add_prop_call_post acc kind called_kf bhv tkind ~assumes post =
let add_prop_assert acc kind kf s ca p =
let id = WpPropId.mk_assert_id kf s ca in
- let labels = NormAtLabels.labels_assert_before ~kf s in
+ let labels = NormAtLabels.labels_assert ~kf s in
let p = normalize id labels p in
add_prop acc kind id p
--
GitLab