module CtrlDpds:sig
..end
Internal information about control dependencies
val dkey : Log.category
module Lexical_successors:sig
..end
module PdgPostdom:sig
..end
typet =
Lexical_successors.t * PdgPostdom.t
val compute : Cil_types.kernel_function ->
Lexical_successors.t * PdgPostdom.t
val pd_b_but_not_a : PdgPostdom.t ->
Cil_types.stmt -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t
({B} U postdom(B))-postdom(A). It means that if S is in the result, it postdominates B but not A. As B is usually a successor of A, it means that S is reached if the B-branch is chosen, but not necessary for the other branches. Then, S should depend on A. (see the document to know more about the applied algorithm)
val get_if_controled_stmts : 'a * PdgPostdom.t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t
= U (PDB (if, succs(if))(see the document to know more about the applied algorithm).
val jump_controled_stmts : PdgPostdom.t ->
Cil_types.stmt ->
Cil_types.stmt -> Cil_datatype.Stmt.Hptset.elt -> Cil_datatype.Stmt.Hptset.t
val get_jump_controled_stmts : Lexical_successors.t * PdgPostdom.t ->
Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t
PDB(jump,lex_suc) U (PDB(lex_suc,label) - lex_suc)(see the document to know more about the applied algorithm).
Compute the list of the statements that should have a control dependency
on the given jump statement. This statement can be a goto
of course,
but also a break
, a continue
, or even a loop because CIL transformations
make them of the form
while(true) body;which is equivalent to
L : body ; goto L;
val get_loop_controled_stmts : Lexical_successors.t * PdgPostdom.t ->
Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t
while(1) S; LS:
as L: S; goto L; LS: