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_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.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c.kernel/Frama_c_kernel/Cfg/index.html

Module `Frama_c_kernel.Cfg`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c.kernel/Frama_c_kernel/Cfg/index.html

Module Frama_c_kernel.Cfg

Module `Frama_c_kernel.Cfg`