From 5f7ced90f91d335586ff525c0aa2a64c1b40f14e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 13 Jan 2021 16:23:55 +0100
Subject: [PATCH] [wp] remove useless parameter in W.use_assigns
---
src/plugins/wp/calculus.ml | 8 ++++----
src/plugins/wp/cfgDump.ml | 2 +-
src/plugins/wp/cfgWP.ml | 4 ++--
src/plugins/wp/mcfg.ml | 4 ++--
4 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index ba69ffcc2a1..a60663c67ed 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -76,12 +76,12 @@ module Cfg (W : Mcfg.S) = struct
let add_assigns_hyp wenv obj h_assigns = match h_assigns with
| WpPropId.AssignsLocations (h_id, a) ->
let hid = Some h_id in
- let obj = W.use_assigns wenv a.WpPropId.a_stmt hid a obj in
+ let obj = W.use_assigns wenv hid a obj in
Some a.WpPropId.a_label, obj
| WpPropId.AssignsAny a ->
Wp_parameters.warning ~current:true ~once:true
"Missing assigns clause (assigns 'everything' instead)" ;
- let obj = W.use_assigns wenv a.WpPropId.a_stmt None a obj in
+ let obj = W.use_assigns wenv None a obj in
Some a.WpPropId.a_label, obj
| WpPropId.NoAssignsInfo -> None, obj
@@ -476,7 +476,7 @@ module Cfg (W : Mcfg.S) = struct
| (Set (lv, e, _)) -> W.assign wenv s lv e obj
| (Asm _) ->
let asm = WpPropId.mk_asm_assigns_desc s in
- W.use_assigns wenv asm.WpPropId.a_stmt None asm obj
+ W.use_assigns wenv None asm obj
| (Call _) -> assert false
| Skip _ | Code_annot _ -> obj
end
@@ -652,7 +652,7 @@ module Cfg (W : Mcfg.S) = struct
let obj =
if WpStrategy.isInitConst ()
then process_global_const wenv obj else obj in
- let obj = W.use_assigns wenv None None WpPropId.mk_init_assigns obj in
+ let obj = W.use_assigns wenv None WpPropId.mk_init_assigns obj in
let obj = W.label wenv None Clabels.init obj in
compute_global_init wenv `All obj
end
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index 6091b24dc5a..24d85bc4505 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -124,7 +124,7 @@ struct
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
- let use_assigns _env _stmt region d k =
+ let use_assigns _env region d k =
let u = node () in
begin match region with
| None ->
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index fd9f7e1d959..d8d221d9cbd 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -598,9 +598,9 @@ struct
let sequence = { pre=s0 ; post=s1 } in
sequence , assigned
- let use_assigns wenv stmt hpid ainfo wp = in_wenv wenv wp
+ let use_assigns wenv hpid ainfo wp = in_wenv wenv wp
begin fun env wp ->
- assert (stmt == ainfo.a_stmt) ;
+ let stmt = ainfo.a_stmt in
match ainfo.a_assigns with
| WritesAny ->
diff --git a/src/plugins/wp/mcfg.ml b/src/plugins/wp/mcfg.ml
index 873001be1eb..5fd7743b59c 100644
--- a/src/plugins/wp/mcfg.ml
+++ b/src/plugins/wp/mcfg.ml
@@ -73,8 +73,8 @@ module type S = sig
(** [use_assigns env hid kind assgn goal] performs the havoc on the goal.
* [hid] should be [None] iff [assgn] is [WritesAny],
* and tied to the corresponding identified_property otherwise.*)
- val use_assigns : t_env -> stmt option -> WpPropId.prop_id option ->
- WpPropId.assigns_desc -> t_prop -> t_prop
+ val use_assigns : t_env ->
+ WpPropId.prop_id option -> WpPropId.assigns_desc -> t_prop -> t_prop
val label : t_env -> stmt option -> Clabels.c_label -> t_prop -> t_prop
val init : t_env -> varinfo -> init option -> t_prop -> t_prop
--
GitLab