[wp] remove useless parameter in W.use_assigns

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

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 ->

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 ->

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