diff --git a/src/plugins/wp/clabels.ml b/src/plugins/wp/clabels.ml
index f9e26a0db028f01cb19e437f3fc277cacd4f1fd5..6f20a911f5e0d72a362203299f8de5421274d1d9 100644
--- a/src/plugins/wp/clabels.ml
+++ b/src/plugins/wp/clabels.ml
@@ -59,6 +59,7 @@ let mem l lbl = List.mem l lbl
 
 let case n = "wp:case" ^ Int64.to_string n
 let stmt s = "wp:sid"  ^ string_of_int s.sid
+let stmt_post s = "wp:sid:post:" ^ string_of_int s.sid
 let loop_entry s = stmt s (* same point *)
 let loop_current s = "wp:head" ^ string_of_int s.sid
 
diff --git a/src/plugins/wp/clabels.mli b/src/plugins/wp/clabels.mli
index 33812ec5f1377b696943adbbdfbd50cb110555cf..4014aab7f58b4fbd571688c255b2ffe684b7b2e2 100644
--- a/src/plugins/wp/clabels.mli
+++ b/src/plugins/wp/clabels.mli
@@ -56,6 +56,7 @@ val formal : string -> c_label
 
 val case : int64 -> c_label
 val stmt : Cil_types.stmt -> c_label
+val stmt_post : Cil_types.stmt -> c_label
 val loop_entry : Cil_types.stmt -> c_label
 val loop_current : Cil_types.stmt -> c_label
 
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index 197b12f968517c08056b5183ade17088df4863a3..fb30f63eadddcb4623e9fdca28c3065744904d2c 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -153,12 +153,24 @@ let labels_stmt_pre ~kf s = function
   | BuiltinLabel Here -> Clabels.stmt s
   | l -> labels_fct ~kf ~at:s l
 
-let labels_stmt_post ~kf s l_post = function
+let labels_stmt_post ~kf s = function
+  | BuiltinLabel Old -> Clabels.stmt s
+  | BuiltinLabel (Here | Post) -> Clabels.stmt_post s
+  | l -> labels_fct ~kf ~at:s l
+
+let labels_stmt_assigns ~kf s = function
+  | BuiltinLabel (Here | Old) -> Clabels.stmt s
+  | BuiltinLabel Post -> Clabels.stmt_post s
+  | l -> labels_fct ~kf ~at:s l
+
+(* LEGACY *)
+let labels_stmt_post_l ~kf s l_post = function
   | BuiltinLabel Old -> Clabels.stmt s
   | BuiltinLabel (Here | Post) as l -> option l l_post
   | l -> labels_fct ~kf ~at:s l
 
-let labels_stmt_assigns ~kf s l_post = function
+(* LEGACY *)
+let labels_stmt_assigns_l ~kf s l_post = function
   | BuiltinLabel (Here | Old) -> Clabels.stmt s
   | BuiltinLabel Post as l -> option l l_post
   | l -> labels_fct ~kf ~at:s l
diff --git a/src/plugins/wp/normAtLabels.mli b/src/plugins/wp/normAtLabels.mli
index 0dd24f825450e8170399fcf7ab9f0de90b6fd320..2becd6c715a6c6438479c4567241e5bdc8438b31 100644
--- a/src/plugins/wp/normAtLabels.mli
+++ b/src/plugins/wp/normAtLabels.mli
@@ -36,8 +36,10 @@ 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_loop : stmt -> label_mapping
 val labels_stmt_pre : kf:kernel_function -> stmt -> label_mapping
-val labels_stmt_post : kf:kernel_function -> stmt -> c_label option -> label_mapping
-val labels_stmt_assigns : kf:kernel_function -> stmt -> c_label option -> label_mapping
+val labels_stmt_post : kf:kernel_function -> stmt -> label_mapping
+val labels_stmt_assigns : kf:kernel_function -> stmt -> label_mapping
+val labels_stmt_post_l : kf:kernel_function -> stmt -> c_label option -> label_mapping
+val labels_stmt_assigns_l : kf:kernel_function -> stmt -> c_label option -> label_mapping
 val labels_predicate : (logic_label * logic_label) list -> label_mapping
 val labels_axiom : label_mapping
 
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 88708e985e55d6cf6ab33d725109134b4894939b..63b388971496864ce09f779509cf621abfea26e8 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -188,6 +188,47 @@ let preconditions_at_call s = function
 let get_called_preconditions_at kf stmt =
   List.map snd (call_preconditions kf stmt)
 
+(* -------------------------------------------------------------------------- *)
+(* --- Property Accessors : Behaviors                                     --- *)
+(* -------------------------------------------------------------------------- *)
+
+type behavior = {
+  bhv_assumes: WpPropId.pred_info list ;
+  bhv_requires: WpPropId.pred_info list ;
+  bhv_ensures: WpPropId.pred_info list ;
+  bhv_exits: WpPropId.pred_info list ;
+  bhv_assigns: WpPropId.assigns_full_info list ;
+}
+
+let get_behavior kf ki bhv =
+  let module L = NormAtLabels in
+  let normalize_pre ip =
+    let labels =
+      match ki with
+      | Kglobal -> L.labels_fct_pre
+      | Kstmt s -> L.labels_stmt_pre kf s in
+    WpPropId.mk_pre_id kf ki bhv ip ,
+    L.preproc_annot labels ip.ip_content.tp_statement
+  in
+  let normalize_post tk ip =
+    let labels =
+      match ki with
+      | Kglobal -> L.labels_fct_pre
+      | Kstmt s -> L.labels_stmt_post kf s in
+    WpPropId.mk_post_id kf ki bhv (tk,ip) ,
+    L.preproc_annot labels ip.ip_content.tp_statement
+  in
+  let post_cond tk = List.filter_map (fun (kind,ip) ->
+      if kind = tk then Some (normalize_post tk ip) else None
+    ) bhv.b_post_cond
+  in {
+    bhv_assumes = List.map normalize_pre bhv.b_assumes;
+    bhv_requires = List.map normalize_pre bhv.b_requires;
+    bhv_ensures = post_cond Normal ;
+    bhv_exits = post_cond Exits ;
+    bhv_assigns = [];
+  }
+
 (* -------------------------------------------------------------------------- *)
 (* --- Code Assertions                                                    --- *)
 (* -------------------------------------------------------------------------- *)
@@ -517,7 +558,7 @@ let add_stmt_assigns_goal config s active acc b l_post = match b.b_assigns with
       | Some id ->
           if goal_to_select config id then
             let kf = config.kf in
-            let labels = NormAtLabels.labels_stmt_assigns ~kf s l_post in
+            let labels = NormAtLabels.labels_stmt_assigns_l ~kf s l_post in
             let assigns = NormAtLabels.preproc_assigns labels assigns in
             let a_desc = WpPropId.mk_stmt_assigns_desc s assigns in
             WpStrategy.add_assigns acc WpStrategy.Agoal id a_desc
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index daaf415162ecef6133a28f23d20eaada8bf8f41c..38d2dcbdcfab529a16f8f6635f009460a8dfbfa5 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -63,6 +63,20 @@ val get_called_post_conditions : kernel_function -> Property.t list
 val get_called_exit_conditions : kernel_function -> Property.t list
 val get_called_assigns : kernel_function -> Property.t list
 
+(* -------------------------------------------------------------------------- *)
+(* --- Property Accessors : Behaviors                                     --- *)
+(* -------------------------------------------------------------------------- *)
+
+type behavior = {
+  bhv_assumes: WpPropId.pred_info list ;
+  bhv_requires: WpPropId.pred_info list ;
+  bhv_ensures: WpPropId.pred_info list ;
+  bhv_exits: WpPropId.pred_info list ;
+  bhv_assigns: WpPropId.assigns_full_info list;
+}
+
+val get_behavior : kernel_function -> kinstr -> funbehavior -> behavior
+
 (* -------------------------------------------------------------------------- *)
 (* --- Property Accessors : Assertions                                    --- *)
 (* -------------------------------------------------------------------------- *)
@@ -91,6 +105,8 @@ type loop_contract = {
 
 val get_loop_contract : kernel_function -> stmt -> loop_contract
 
+(* -------------------------------------------------------------------------- *)
+
 (* ########################################################################## *)
 (* ###      WARNING:  DEPRECATED API BELOW THIS LINE                      ### *)
 (* ########################################################################## *)
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index a95b4a864909dffb1047d8539b10948a51d73d00..9097438fdcb40a7837f298a880465a24be652c20 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -169,6 +169,9 @@ let mk_fct_assigns_id kf b tkind a =
 let mk_pre_id kf ki b p =
   mk_prop PKProp (Property.ip_of_requires kf ki b p)
 
+let mk_post_id kf ki b p =
+  mk_prop PKProp (Property.ip_of_ensures kf ki b p)
+
 let mk_stmt_post_id kf s b p =
   mk_prop PKProp (Property.ip_of_ensures kf (Kstmt s) b p)
 
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 29098180bbefd8e1aff6209038722fc25eb84660..c3adc45404bcb9750459a0c67ca4853ef68f4c14 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -183,6 +183,9 @@ val mk_fct_assigns_id : kernel_function -> funbehavior ->
 val mk_pre_id : kernel_function -> kinstr -> funbehavior ->
   identified_predicate -> prop_id
 
+val mk_post_id : kernel_function -> kinstr -> funbehavior ->
+  termination_kind * identified_predicate -> prop_id
+
 val mk_stmt_post_id : kernel_function -> stmt -> funbehavior ->
   termination_kind * identified_predicate -> prop_id
 
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index 7026d2402035f301bee12cf740d9b92663f712f0..195affa7997046ebeebe75c3b00e2d8c1ca733ae 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -228,7 +228,7 @@ let add_prop_stmt_spec_pre acc kind kf s spec =
 
 let add_prop_stmt_post acc kind kf s bhv tkind l_post ~assumes post =
   let id = WpPropId.mk_stmt_post_id kf s bhv (tkind, post) in
-  let labels = NormAtLabels.labels_stmt_post ~kf s l_post in
+  let labels = NormAtLabels.labels_stmt_post_l ~kf s l_post in
   let p = Logic_const.pred_of_id_pred post in
   let p = normalize id labels ?assumes p in
   add_prop acc kind id p
@@ -403,7 +403,7 @@ let add_stmt_spec_assigns_hyp acc kf s l_post spec =
       | None -> add_assigns_any acc Ahyp
                   (WpPropId.mk_stmt_any_assigns_info s)
       | Some id ->
-          let labels = NormAtLabels.labels_stmt_assigns ~kf s l_post in
+          let labels = NormAtLabels.labels_stmt_assigns_l ~kf s l_post in
           let assigns = NormAtLabels.preproc_assigns labels assigns in
           let a_desc = WpPropId.mk_stmt_assigns_desc s assigns in
           add_assigns acc Ahyp id a_desc
@@ -432,7 +432,7 @@ let add_call_assigns_hyp acc kf_caller s ~called_kf l_post spec_opt =
               add_assigns_any acc (AcallHyp called_kf) asgn
           | Some pid ->
               let kf = kf_caller in
-              let labels = NormAtLabels.labels_stmt_assigns ~kf s l_post in
+              let labels = NormAtLabels.labels_stmt_assigns_l ~kf s l_post in
               let assigns = NormAtLabels.preproc_assigns labels assigns in
               let a_desc = WpPropId.mk_stmt_assigns_desc s assigns in
               add_assigns acc (AcallHyp called_kf) pid a_desc