Module CtrlDpds

module CtrlDpds: sig .. end

Internal information about control dependencies


type t 
val compute : Kernel_function.t -> t

Compute some information on the function in order to be able to compute the control dependencies later on

val get_if_controlled_stmts : t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t

Compute the list of the statements that should have a control dependency on the given IF statement.

val get_jump_controlled_stmts : t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t

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;

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_controlled_stmts : t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t

Try to process while(1) SLS as LS; goto LLS