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