Module type Dataflow.ForwardsTransfer

module type ForwardsTransfer = sig .. end

val name : string

For debugging purposes, the name of the analysis

val debug : bool Pervasives.ref

Whether to turn on debugging

type t 

The type of the data we compute for each block start. May be imperative.

val copy : t -> t

Make a deep copy of the data.

val pretty : Format.formatter -> t -> unit

Pretty-print the state.

val computeFirstPredecessor : Cil_types.stmt -> t -> t

computeFirstPredecessor s d is called when s is reached for the first time (i.e. no previous data is associated with it). The data d is propagated to s from an unspecified preceding statement s'. The result of the call is stored as the new data for s.

computeFirstPredecessor usually leaves d unchanged, but may potentially change it. It is also possible to perform a side-effect, for dataflows that store information out of the type t.

val combinePredecessors : Cil_types.stmt ->
       old:t ->
       t -> t option

Take some old data for the given statement, and some new data for the same point. Return None if the combination is identical to the old data, to signify that a fixpoint is currently reached for this statement. Otherwise, compute the combination, and return it.

val doInstr : Cil_types.stmt ->
       Cil_types.instr ->
       t -> t Dataflow.action

The (forwards) transfer function for an instruction (which is englobed by the given statement). The action Default propagates the state passed as an argument unchanged. The current location is updated before this function is called.

val doGuard : Cil_types.stmt ->
       Cil_types.exp ->
       t ->
       t Dataflow.guardaction *
       t Dataflow.guardaction

Generate the successors act_th, act_el to an If statement. act_th (resp. act_el) corresponds to the case where the given expression evaluates to zero (resp. non-zero). It is always possible to return GDefault, GDefault, especially for analyses that do not use guard information. This is equivalent to returning GUse d, GUse d, where d is the input state. A return value of GUnreachable indicates that this half of the branch will not be taken and should not be explored. stmt is the corresponding If statement, passed as information only.

val doStmt : Cil_types.stmt ->
       t ->
       t Dataflow.stmtaction

The (forwards) transfer function for a statement. The (Cil.CurrentLoc.get ()) * is set before calling this. The default action is to do the instructions * in this statement, if applicable, and continue with the successors.

val filterStmt : Cil_types.stmt -> bool

Whether to put this statement in the worklist. This is called when a block would normally be put in the worklist.

val stmt_can_reach : Cil_types.stmt -> Cil_types.stmt -> bool

Must return true if ther is a path in the control-flow graph of the function from the first statement to the second. Used to choose a "good" node in the worklist. Suggested use is let stmt_can_reach = Stmts_graph.stmt_can_reach kf, where kf is the kernel_function being analyzed; let stmt_can_reach _ _ = true is also correct, albeit less efficient

val doEdge : Cil_types.stmt ->
       Cil_types.stmt -> t -> t

what to do when following the edge between the two given statements. Can default to identity if nothing special is required.

module StmtStartData: Dataflow.StmtStartData  with type data = t

For each statement id, the data at the start.