Module GoblintCil.Dataflow

A framework for data flow analysis for CIL code. Before using this framework, you must initialize the Control-flow Graph for your program, e.g using Cfg.computeFileCFG

type 't action =
  1. | Default
    (*

    The default action

    *)
  2. | Done of 't
    (*

    Do not do the default action. Use this result

    *)
  3. | Post of 't -> 't
    (*

    The default action, followed by the given transformer

    *)
type 't stmtaction =
  1. | SDefault
    (*

    The default action

    *)
  2. | SDone
    (*

    Do not visit this statement or its successors

    *)
  3. | SUse of 't
    (*

    Visit the instructions and successors of this statement as usual, but use the specified state instead of the one that was passed to doStmt

    *)
type 't guardaction =
  1. | GDefault
    (*

    The default state

    *)
  2. | GUse of 't
    (*

    Use this data for the branch

    *)
  3. | GUnreachable
    (*

    The branch will never be taken.

    *)
module type ForwardsTransfer = sig ... end
module ForwardsDataFlow (T : ForwardsTransfer) : sig ... end
module type BackwardsTransfer = sig ... end
module BackwardsDataFlow (T : BackwardsTransfer) : sig ... end
val find_stmts : Cil.fundec -> Cil.stmt list * Cil.stmt list

Returns (all_stmts, sink_stmts), where all_stmts is a list of the statements in a function, and sink_stmts is a list of the return statments (including statements that fall through the end of a void function). Useful when you need an initial set of statements for BackwardsDataFlow.compute.