diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 401ee6ebaf9baff67c9179887c36eb10d95821fc..acfdcecd1b6fe560336d8cf0e5b66f7c3e648d6a 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -275,6 +275,18 @@ let get_call_contract ?smoking kf =
       let g = smoke kf ~id:"dead_call" ~unreachable:s () in
       { cc with contract_smoke = [ g ] }
 
+(* -------------------------------------------------------------------------- *)
+(* --- Code Contracts                                                     --- *)
+(* -------------------------------------------------------------------------- *)
+
+let get_code_behaviors stmt =
+  Annotations.fold_code_annot
+    (fun _emitter ca cs ->
+       match ca.annot_content with
+       | AStmtSpec(fors,spec) -> (fors,spec) :: cs
+       | _ -> cs
+    ) stmt []
+
 (* -------------------------------------------------------------------------- *)
 (* --- Code Assertions                                                    --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 88384ea7f7a54e573e036134ac7dd70b5d394564..030bd48749f672414b0c21aefdc387802128939c 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -53,6 +53,12 @@ val get_preconditions : goal:bool -> kernel_function -> pred_info list
 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                                    --- *)
 (* -------------------------------------------------------------------------- *)