[wp] collect code behaviors

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                                                    --- *)
 (* -------------------------------------------------------------------------- *)

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                                    --- *)
 (* -------------------------------------------------------------------------- *)