module Annot:sig
..end
Raises Kernel_function.No_Definition
on annotations for function declarations.
typedata_info =
((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
option
data_info
is composed of (node,z_part) list, undef_loc)
and correspond to data dependencies nodes.
Can be None if we don't know how to compute them.typectrl_info =
PdgTypes.Node.t list
ctrl_info
correspond to control dependancies nodestypedecl_info =
PdgTypes.Node.t list
decl_info
correspond to the declarations nodes of the variables needed to
parse the annotationval find_code_annot_nodes : PdgTypes.Pdg.t ->
Cil_types.stmt ->
Cil_types.code_annotation ->
ctrl_info * decl_info * data_info
Not_found
when the statement is unreachable.val find_fun_precond_nodes : PdgTypes.Pdg.t -> Cil_types.predicate -> decl_info * data_info
val find_fun_postcond_nodes : PdgTypes.Pdg.t -> Cil_types.predicate -> decl_info * data_info
val find_fun_variant_nodes : PdgTypes.Pdg.t -> Cil_types.term -> decl_info * data_info