sig
  val setup_precondition_proxy :
    Cil_types.kernel_function -> Property.t -> unit
  val setup_all_preconditions_proxies : Cil_types.kernel_function -> unit
  val precondition_at_call :
    Cil_types.kernel_function -> Property.t -> Cil_types.stmt -> Property.t
  val all_call_preconditions_at :
    warn_missing:bool ->
    Cil_types.kernel_function ->
    Cil_types.stmt -> (Property.t * Property.t) list
  val all_functions_with_preconditions :
    Cil_types.stmt -> Kernel_function.Hptset.t
  val replace_call_precondition :
    Property.t -> Cil_types.stmt -> Property.t -> unit
end