Module Pdg_state

module Pdg_state: sig .. end

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


exception Cannot_fold

Types data_state and Node.t come froms this module

val make : PdgTypes.LocInfo.t -> Locations.Zone.t -> PdgTypes.data_state
val empty : PdgTypes.data_state
val bottom : PdgTypes.data_state
val add_loc_node : PdgTypes.data_state ->
exact:bool -> Locations.Zone.t -> PdgTypes.Node.t -> PdgTypes.data_state
val add_init_state_input : PdgTypes.data_state ->
Locations.Zone.t -> PdgTypes.Node.t -> 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.

val get_loc_nodes : PdgTypes.data_state ->
Locations.Zone.t ->
(PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option
val pretty : Stdlib.Format.formatter -> PdgTypes.data_state -> unit
type states = PdgTypes.data_state Cil_datatype.Stmt.Hashtbl.t 
val store_init_state : states -> PdgTypes.data_state -> unit
val store_last_state : states -> PdgTypes.data_state -> unit
val get_init_state : states -> PdgTypes.data_state
val get_stmt_state : states -> Cil_types.stmt -> PdgTypes.data_state
val get_last_state : states -> PdgTypes.data_state