module Computer: functor (
Initial
:
sig
end
) ->
Parameters: |
Initial |
: |
sig val initial: (stmt * PdgTypes.data_state) list end
|
Fenv |
: |
Dataflows.FUNCTION_ENV
|
Param |
: |
sig val current_pdg : pdg_build
val ctrl_dpds_infos : CtrlDpds.t
end
|
|
val pdg_debug : ('a, Format.formatter, unit) Pervasives.format -> 'a
type
t = PdgTypes.data_state
val current_pdg : Build.pdg_build
val current_function : Kernel_function.t
val ctrl_dpds_infos : CtrlDpds.t
val init : (Cil_types.stmt * PdgTypes.data_state) list
val bottom : PdgTypes.data_state
val pretty : Format.formatter -> t -> unit
val join_and_is_included : t -> t -> PdgTypes.data_state * bool
val join : t -> t -> PdgTypes.data_state
val doInstr : Cil_types.stmt ->
Cil_types.instr -> PdgTypes.data_state -> PdgTypes.data_state
Compute the new state after 'instr' starting from state before 'state'.
val transfer_stmt : Cil_types.stmt ->
t -> (Cil_types.stmt * t) list
Called before processing the successors of the statements.