Module Annot

module Annot: sig .. end
All these functions find the nodes needed for various kind of annotations.


Raises Kernel_function.No_Definition on annotations for function declarations.


type data_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.
type ctrl_info = PdgTypes.Node.t list 
ctrl_info correspond to control dependancies nodes
type decl_info = PdgTypes.Node.t list 
decl_info correspond to the declarations nodes of the variables needed to parse the annotation
val zone_info_nodes : PdgTypes.Pdg.t ->
Db.Properties.Interp.To_zone.t list option ->
((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
option
val get_decl_nodes : PdgTypes.Pdg.t -> Cil_datatype.Varinfo.Set.t -> PdgTypes.Node.t list
val find_nodes_for_function_contract : PdgTypes.Pdg.t ->
(Kernel_function.t ->
Db.Properties.Interp.To_zone.t list option *
Db.Properties.Interp.To_zone.t_decl) ->
PdgTypes.Node.t list *
((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
option
val find_fun_precond_nodes : PdgTypes.Pdg.t ->
Cil_types.predicate ->
PdgTypes.Node.t list *
((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
option
val find_fun_postcond_nodes : PdgTypes.Pdg.t ->
Cil_types.predicate ->
PdgTypes.Node.t list *
((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
option
val find_fun_variant_nodes : PdgTypes.Pdg.t ->
Cil_types.term ->
PdgTypes.Node.t list *
((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
option
val find_code_annot_nodes : Db.Pdg.t ->
Cil_types.stmt ->
Cil_types.code_annotation ->
PdgTypes.Node.t list * PdgTypes.Node.t list *
((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
option
Raises Not_found when the statement is unreachable.