Module Pdg_state

module Pdg_state: sig .. end
DataState is associated with a program point and provide the dependancies for the data, ie. it stores for each location the nodes of the pdg where its value was last defined.

Types data_state and Node.t come froms this module


val dkey : Log.category
module P: Pdg_parameters
exception Cannot_fold
val make : PdgTypes.LocInfo.t -> Locations.Zone.t -> PdgTypes.data_state
val empty : PdgTypes.data_state
val bottom : PdgTypes.data_state
val pretty : Format.formatter -> PdgTypes.data_state -> unit
val add_loc_node : PdgTypes.data_state ->
?initializing:bool ->
exact:bool ->
Locations.Zone.t -> PdgTypes.NodeSetLattice.O.elt -> PdgTypes.data_state
val add_init_state_input : PdgTypes.data_state ->
Locations.Zone.t -> PdgTypes.NodeSetLattice.O.elt -> PdgTypes.data_state
this one is very similar to add_loc_node except that we want to accumulate the nodes (exact = false) but nonetheless define under_outputs like (exact = true)
val test_and_merge : old:PdgTypes.data_state -> PdgTypes.data_state -> bool * PdgTypes.data_state
Kind of 'join' of the two states but test before if the new state is included in ~old.
Returns (true, old U new) if the result is a new state, (false, old) if new is included in old.
val get_loc_nodes_and_part : PdgTypes.data_state ->
Locations.Zone.t ->
(PdgTypes.NodeSetLattice.O.elt * Locations.Zone.t option) list
returns pairs of (n, z_opt) where n is a node that computes a part of loc and z is the intersection between loc and the zone computed by the node.
Raises Cannot_fold if the state is top (TODO : something better ?)
val get_loc_nodes : PdgTypes.data_state ->
Locations.Zone.t ->
(PdgTypes.NodeSetLattice.O.elt * Locations.Zone.t option) list *
Locations.Zone.t option
Raises Cannot_fold (see get_loc_nodes_and_part)

if the state is Top

type states = PdgTypes.data_state Cil_datatype.Stmt.Hashtbl.t 
val stmt_init : Cil_datatype.Stmt.t
val stmt_last : Cil_types.stmt
val store_init_state : 'a Cil_datatype.Stmt.Hashtbl.t -> 'a -> unit
val store_last_state : 'a Cil_datatype.Stmt.Hashtbl.t -> 'a -> unit
val get_init_state : 'a Cil_datatype.Stmt.Hashtbl.t -> 'a
val get_last_state : 'a Cil_datatype.Stmt.Hashtbl.t -> 'a
val get_stmt_state : 'a Cil_datatype.Stmt.Hashtbl.t -> Cil_datatype.Stmt.Hashtbl.key -> 'a