module CtrlDpds:sig
..end
Lexical successors
type
t
val compute : Kernel_function.t -> t
val get_if_controled_stmts : 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 get_jump_controled_stmts : t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t
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;
let's find the statements which are depending on the jump statement (goto, break, continue) =
PDB(jump,lex_suc) U (PDB(lex_suc,label) - lex_suc)(see the document to know more about the applied algorithm).
val get_loop_controled_stmts : t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t
while(1) S; LS:
as L: S; goto L; LS: