Frama-C:
Plug-ins:
Libraries:

Frama-C API - Cfg

Code to compute the control-flow graph of a function or file. This will fill in the preds and succs fields of Cil_types.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.