diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 8a10e8ec185aea80e2a452f19437a7a05cb13306..b2a6b81c89d2c60913d947393d01d3cf34b958c2 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -268,6 +268,36 @@ let get_kf = function
   | IPOther {io_loc} -> kf_of_loc_o io_loc
   | IPTypeInvariant _ | IPGlobalInvariant _ -> None
 
+let get_ir p =
+  let get_pp = function
+    | IPPredicate {ip_kind = PKRequires _ | PKAssumes _ | PKTerminates }
+    | IPAxiomatic _ | IPLemma _ | IPComplete _ | IPDisjoint _ | IPCodeAnnot _
+    | IPAllocation _ | IPDecrease _ | IPPropertyInstance _ | IPOther _
+    | IPTypeInvariant _ | IPGlobalInvariant _
+      -> Before
+    | IPPredicate _ | IPAssigns _ | IPFrom _ | IPExtended _ | IPBehavior _
+      -> After
+    | IPReachable ir -> ir.ir_program_point
+  in
+  let ir_kf = get_kf p in
+  let ir_kinstr = get_kinstr p in
+  let ir_program_point = get_pp p in
+  {ir_kf; ir_kinstr; ir_program_point}
+
+let get_prog_state p =
+  let ir = get_ir p in
+  match ir.ir_kf, ir.ir_kinstr with
+  | None, _ | _, Kstmt _ -> ir
+  | Some kf, Kglobal ->
+    try
+      let ir_kinstr =
+        if ir.ir_program_point = Before
+        then Kstmt (Kernel_function.find_first_stmt kf)
+        else Kstmt (Kernel_function.find_return kf)
+      in
+      {ir with ir_kinstr}
+    with Kernel_function.No_Statement -> ir
+
 let rec get_names = function
   | IPPredicate ip -> (Logic_const.pred_of_id_pred ip.ip_pred).pred_name
   | IPExtended { ie_ext = {ext_name = name} }
@@ -1271,23 +1301,9 @@ let ip_other io_name io_loc = IPOther {io_name; io_loc}
 let ip_reachable_stmt kf ki =
   IPReachable {ir_kf=Some kf; ir_kinstr=Kstmt ki; ir_program_point=Before}
 
-let ip_reachable_ppt p =
-  let ir_kf = get_kf p in
-  let ir_kinstr = get_kinstr p in
-  let ir_program_point = match p with
-    | IPPredicate {ip_kind=(PKRequires _ | PKAssumes _ | PKTerminates)}
-    | IPAxiomatic _ | IPLemma _ | IPComplete _
-    | IPDisjoint _ | IPCodeAnnot _ | IPAllocation _
-    | IPDecrease _ | IPPropertyInstance _ | IPOther _
-    | IPTypeInvariant _ | IPGlobalInvariant _
-      -> Before
-    | IPPredicate _ | IPAssigns _ | IPFrom _
-    | IPExtended _
-    | IPBehavior _
-      -> After
-    | IPReachable _ -> Kernel.fatal "IPReachable(IPReachable _) is not possible"
-  in
-  IPReachable {ir_kf; ir_kinstr; ir_program_point}
+let ip_reachable_ppt = function
+  | IPReachable _ -> Kernel.fatal "IPReachable(IPReachable _) is not possible"
+  | p -> IPReachable (get_ir p)
 
 let ip_of_ensures ip_kf ip_kinstr b (k,ip_pred) =
   IPPredicate {ip_kind=PKEnsures (b, k); ip_kf; ip_kinstr; ip_pred}
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 0ba0230c246577602eb725c0b37c0e08a6a28e89..1fc7d1d7ddedf6fc0a71f34cf136dbb33d30c2d6 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -127,8 +127,9 @@ type identified_reachable = {
   ir_program_point : program_point
 }
 (** [None, Kglobal] --> global property
-    [None, Some ki] --> impossible
-    [Some kf, Kglobal] --> property of a function without code
+    [None, Kstmt stmt] --> impossible
+    [Some kf, Kglobal] -->
+      property of a function without code / Not directly attached to a statement
     [Some kf, Kstmt stmt] --> reachability of the given stmt (and the attached
     properties) *)
 
@@ -503,6 +504,19 @@ val has_status: identified_property -> bool
 
 val get_kinstr: identified_property -> kinstr
 val get_kf: identified_property -> kernel_function option
+
+val get_ir: identified_property -> identified_reachable
+(** For a given property, returns its corresponding [kernel_function], [kinstr]
+    and program point.
+    @since Frama-C+dev *)
+
+val get_prog_state: identified_property -> identified_reachable
+(** Uses [get_ir]. If [ir_kf] is [Some kf] and [ir_kinstr] is
+    [Kglobal], we try to attach a statement depending on [ir_program_point] :
+    the first statement of [kf] for [Before], the return statement of kf for
+    [After].
+    @since Frama-C+dev *)
+
 val get_behavior: identified_property -> funbehavior option
 val get_names: identified_property -> string list
 val get_for_behaviors: identified_property -> string list