From bc0ce693008a682bc29ffaef2489d2a055fd606c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 11 Feb 2021 12:33:00 +0100
Subject: [PATCH] [wp] collect code behaviors
---
src/plugins/wp/cfgAnnot.ml | 12 ++++++++++++
src/plugins/wp/cfgAnnot.mli | 6 ++++++
2 files changed, 18 insertions(+)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 401ee6ebaf9..acfdcecd1b6 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 88384ea7f7a..030bd48749f 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 --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab