package goblint-cil

  1. Overview
  2. Docs

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 required for several other extensions, such as Dataflow.

val computeFileCFG : Cil.file -> unit

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

val clearFileCFG : Cil.file -> unit

clear the sid, succs, and preds fields of each statement.

val cfgFun : Cil.fundec -> int

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

val clearCFGinfo : Cil.fundec -> unit

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

val printCfgChannel : out_channel -> Cil.fundec -> unit

print control flow graph (in dot form) for fundec to channel

val printCfgFilename : string -> Cil.fundec -> unit

Print control flow graph (in dot form) for fundec to file

val start_id : int ref

Next statement id that will be assigned.

val allStmts : Cil.file -> Cil.stmt list

Return all statements in a file - valid after computeFileCfg only

OCaml

Innovation. Community. Security.