Wpo.generator
method compute_ip : Frama_c_kernel.Property.t -> t Frama_c_kernel.Bag.t
Generate VCs for call preconditions at the given statement.
method compute_call : Frama_c_kernel.Cil_types.stmt -> t Frama_c_kernel.Bag.t
Generate VCs for all functions matching provided behaviors and property names. For `~bhv` and `~prop` optional arguments, default and empty list means all properties.
method compute_main : ?fct:Wp__.Wp_parameters.functions ->
?bhv:string list ->
?prop:string list ->
unit ->
t Frama_c_kernel.Bag.t