Wp.WpTarget
This module computes the set of kernel functions that are considered by the command line options transmitted to WP. That is:
It takes in account the options -wp-bhv and -wp-props so that if all functions are initially selected but in fact some of them are filtered out by these options, they are not considered.
val compute :
WpContext.model ->
?fct:Wp_parameters.functions ->
?bhv:string list ->
?prop:string list ->
unit ->
unit
Compute the entire set, populating specification related to:
val compute_kf : WpContext.model -> Frama_c_kernel.Kernel_function.t -> unit
Compute the target properties associated to the given kernel function. It also populates exits, terminates and assigns for the function and its callees, as well as RTE assertions if they are asked on command line.
val iter : (Frama_c_kernel.Kernel_function.t -> unit) -> unit
val with_callees :
Frama_c_kernel.Kernel_function.t ->
Frama_c_kernel.Kernel_function.Set.t