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 -> unit
setup_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 -> unit
setup_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.t
property_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) list
all_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.t
Returns 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 -> unit
replace_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