package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

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

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.