Module type Dataflow.ForwardsTransfer

module type ForwardsTransfer = sig .. end

val name : string

For debugging purposes, the name of the analysis

val debug : bool Stdlib.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 stmtStartData : t Inthash.t

For each statement id, the data at the start. Not found in the hash table means nothing is known about the state at this point. At the end of the analysis this means that the block is not reachable.

val pretty : unit -> t -> Pretty.doc

Pretty-print the state

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

Give the first value for a predecessors, compute the value to be set for the block

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

Take some old data for the start of a statement, and some new data for the same point. Return None if the combination is identical to the old data. Otherwise, compute the combination, and return it.

val doInstr : Cil.instr ->
       t -> t Dataflow.action

The (forwards) transfer function for an instruction. The Cil.currentLoc is set before calling this. The default action is to continue with the state unchanged.

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

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

val doGuard : Cil.exp ->
       t ->
       t Dataflow.guardaction

Generate the successor to an If statement assuming the given expression is nonzero. Analyses that don't need guard information can return GDefault; this is equivalent to returning GUse of the input. A return value of GUnreachable indicates that this half of the branch will not be taken and should not be explored. This will be called twice per If, once for "then" and once for "else".

val filterStmt : Cil.stmt -> bool

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