module Statuses_by_call:sig..end
Statuses of preconditions specialized at a given call-point.
val setup_precondition_proxy : Cil_types.kernel_function -> Property.t -> unitsetup_precondition_proxy kf p creates a new property for p
at each syntactic call site of kf, representing the status
of p at this particular call. p is considered proven if and
only if all its instances are themselves proven.
val setup_all_preconditions_proxies : Cil_types.kernel_function -> unitsetup_all_preconditions_proxies kf is equivalent to calling
setup_precondition_proxy on all the requires of kf.
val precondition_at_call : Cil_types.kernel_function -> Property.t -> Cil_types.stmt -> Property.tproperty_at_call kf p stmt returns the property corresponding to the
status of the precondition p at the call stmt. If stmt is a call
through a pointer, the property at this call is created automatically
if needed. For direct calls, setup_precondition_proxy must have been
called before.
val all_call_preconditions_at : warn_missing:bool ->
Cil_types.kernel_function -> Cil_types.stmt -> (Property.t * Property.t) listall_call_preconditions_at create kf stmt returns the copies of all the
requires of kf for the call statement at stmt. The first property in
the tuple is the require, the second the copy at the call point.
If warn_missing is true and a copy has not yet been created an error
is raised.
val all_functions_with_preconditions : Cil_types.stmt -> Kernel_function.Hptset.tReturns the set of functions that can be called at the given statement
and for which a precondition has been specialized at this call.
Those functions are registered when the function Statuses_by_call.precondition_at_call
is called.
val replace_call_precondition : Property.t -> Cil_types.stmt -> Property.t -> unitreplace_for_call pre stmt pre_at_call states that pre_at_call
is the property corresponding to the status of pre at call stmt.
The previous property, if any, is removed. Beware that this may also
remove some already proved statuses