Module Frama_c_kernel.Cfg

Code to compute the control-flow graph of a function or file. This will fill in the preds and succs fields of Cil.stmt

This is nearly always automatically done by the kernel. You only need those functions if you build Cil_types.fundec yourself.

val computeFileCFG : Cil_types.file -> unit

Compute the CFG for an entire file, by calling cfgFun on each function.

val clearFileCFG : ?clear_id:bool -> Cil_types.file -> unit

clear the sid (except when clear_id is explicitly set to false), succs, and preds fields of each statement.

val cfgFun : Cil_types.fundec -> unit

Compute a control flow graph for fd. Stmts in fd have preds and succs filled in

val clearCFGinfo : ?clear_id:bool -> Cil_types.fundec -> unit

clear the sid, succs, and preds fields of each statement in a function

val prepareCFG : ?keepSwitch:bool -> Cil_types.fundec -> unit

This function converts all Break, Switch, Default and Continue Cil_types.stmtkinds and Cil_types.labels into Ifs and Gotos, giving the function body a very CFG-like character. This function modifies its argument in place.