diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index b99158d3cd298b38ead9be6613e20ccd7949856b..84ab16c03bea80c6407a6aede5360c3416569127 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -127,41 +127,6 @@ let is_proved pf =
 let is_invalid pf =
   pf.invalid && not (is_proved pf)
 
-(* -------------------------------------------------------------------------- *)
-(* --- Function Contracts                                                 --- *)
-(* -------------------------------------------------------------------------- *)
-
-(* Properties for kf-conditions of termination-kind 'tkind' *)
-let get_called_postconds (tkind:termination_kind) kf =
-  let bhvs = Annotations.behaviors kf in
-  List.fold_left
-    (fun properties bhv ->
-       List.fold_left
-         (fun properties postcond ->
-            if tkind = fst postcond then
-              let pid_spec = Property.ip_of_ensures kf Kglobal bhv postcond in
-              pid_spec :: properties
-            else properties)
-         properties bhv.b_post_cond)
-    []
-    bhvs
-
-let get_called_post_conditions = get_called_postconds Cil_types.Normal
-let get_called_exit_conditions = get_called_postconds Cil_types.Exits
-
-(** Properties for assigns of kf *)
-let get_called_assigns kf =
-  let bhvs = Annotations.behaviors kf in
-  List.fold_left
-    (fun properties bhv ->
-       if Cil.is_default_behavior bhv then
-         match Property.ip_assigns_of_behavior kf Kglobal [] bhv with
-         | None -> properties
-         | Some ip -> ip :: properties
-       else properties)
-    []
-    bhvs
-
 (* -------------------------------------------------------------------------- *)
 (* --- Preconditions at Callsites                                         --- *)
 (* -------------------------------------------------------------------------- *)
@@ -185,9 +150,6 @@ let preconditions_at_call s = function
       List.map aux preconds
   | Cil2cfg.Dynamic _ -> []
 
-let get_called_preconditions_at kf stmt =
-  List.map snd (call_preconditions kf stmt)
-
 (* -------------------------------------------------------------------------- *)
 (* --- Property Accessors : Behaviors                                     --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index 74f2c0d972d9393f549fc8c1d02f010b51e5cc4b..aee06d48536c4f057be13a4d17b9e609a28d5113 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -55,15 +55,6 @@ val dependencies : proof -> Property.t list
 
 val filter_status : prop_id -> bool
 
-(* -------------------------------------------------------------------------- *)
-(* --- Property Accessors : Function Calls                                --- *)
-(* -------------------------------------------------------------------------- *)
-
-val get_called_preconditions_at : kernel_function -> stmt -> Property.t list
-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                                     --- *)
 (* -------------------------------------------------------------------------- *)