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