diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 7406feddfd24a0420dfc1465e4b1b5f9bbb762b5..84691e71a86c85f545d00d1cdc29105822b72895 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -90,10 +90,10 @@ let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
 
 let normalize_froms tk froms =
   let module L = NormAtLabels in
-  let labels = L.labels_fct_post ~exit:(tk=Exits) in
+  let labels = L.labels_fct_assigns ~exit:(tk=Exits) in
   L.preproc_assigns labels froms
 
-let normalize_assigns kf ~exits bhv = function
+let normalize_fct_assigns kf ~exits bhv = function
   | WritesAny ->
       WpPropId.empty_assigns_info, WpPropId.empty_assigns_info
   | Writes froms ->
@@ -111,7 +111,7 @@ let normalize_assigns kf ~exits bhv = function
 let get_behavior_goals kf ?(smoking=false) ?(exits=false) bhv =
   let pre_cond = normalize_pre ~goal:false kf bhv in
   let post_cond = normalize_post ~goal:true kf bhv in
-  let p_asgn, e_asgn = normalize_assigns kf ~exits bhv bhv.b_assigns in
+  let p_asgn, e_asgn = normalize_fct_assigns kf ~exits bhv bhv.b_assigns in
   let smokes =
     if smoking && bhv.b_requires <> [] then
       let bname =
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index a35c27bf6f6b6e44ceab7059c392619e6fd60ab4..ede64b3bfbf1b7139f57c5698edab7d78a9ce84d 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -56,12 +56,6 @@ val get_behavior_goals :
 val get_complete_behaviors : kernel_function -> pred_info list
 val get_disjoint_behaviors : kernel_function -> pred_info list
 
-(* -------------------------------------------------------------------------- *)
-(* --- Property Accessors : Code Behaviors                                --- *)
-(* -------------------------------------------------------------------------- *)
-
-val get_code_behaviors : stmt -> (string list * funspec) list
-
 (* -------------------------------------------------------------------------- *)
 (* --- Property Accessors : Assertions                                    --- *)
 (* -------------------------------------------------------------------------- *)
@@ -74,7 +68,8 @@ type code_assertions = {
 val get_code_assertions :
   ?smoking:bool -> kernel_function -> stmt -> code_assertions
 
-val get_unreachable : kernel_function -> stmt -> WpPropId.prop_id
+val get_unreachable : kernel_function -> stmt -> prop_id
+val get_stmt_assigns : kernel_function -> stmt -> assigns_full_info list
 
 (* -------------------------------------------------------------------------- *)
 (* --- Property Accessors : Loop Contracts                                --- *)
@@ -82,15 +77,15 @@ val get_unreachable : kernel_function -> stmt -> WpPropId.prop_id
 
 type loop_contract = {
   (** to be verified at loop entry *)
-  loop_established: WpPropId.pred_info list;
+  loop_established: pred_info list;
   (** to be assumed for loop current *)
-  loop_invariants: WpPropId.pred_info list;
+  loop_invariants: pred_info list;
   (** to be proved after loop invariants *)
-  loop_smoke: WpPropId.pred_info list;
+  loop_smoke: pred_info list;
   (** to be verified after loop body *)
-  loop_preserved: WpPropId.pred_info list;
+  loop_preserved: pred_info list;
   (** assigned by loop body *)
-  loop_assigns: WpPropId.assigns_full_info list;
+  loop_assigns: assigns_full_info list;
 }
 
 val get_loop_contract : ?smoking:bool ->