package goblint-cil

  1. Overview
  2. Docs

Module type Dataflow.BackwardsTransferSource

Sourceval name : string

For debugging purposes, the name of the analysis

Sourceval debug : bool ref

Whether to turn on debugging

Sourcetype t

The type of the data we compute for each block start. In many * presentations of backwards data flow analysis we maintain the * data at the block end. This is not easy to do with JVML because * a block has many exceptional ends. So we maintain the data for * the statement start.

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

Pretty-print the state

Sourceval stmtStartData : t Inthash.t

For each block id, the data at the start. This data structure must be * initialized with the initial data for each block

Sourceval funcExitData : t

The data at function exit. Used for statements with no successors. This is usually bottom, since we'll also use doStmt on Return statements.

Sourceval combineStmtStartData : Cil.stmt -> old:t -> t -> t option

When the analysis reaches the start of a block, combine the old data * with the one we have just computed. Return None if the combination is * the same as the old data, otherwise return the combination. In the * latter case, the predecessors of the statement are put on the working * list.

Sourceval combineSuccessors : t -> t -> t

Take the data from two successors and combine it

Sourceval doStmt : Cil.stmt -> t action

The (backwards) transfer function for a branch. The Cil.currentLoc is * set before calling this. If it returns None, then we have some default * handling. Otherwise, the returned data is the data before the branch * (not considering the exception handlers)

Sourceval doInstr : Cil.instr -> t -> t action

The (backwards) transfer function for an instruction. The * Cil.currentLoc is set before calling this. If it returns None, then we * have some default handling. Otherwise, the returned data is the data * before the branch (not considering the exception handlers)

Sourceval filterStmt : Cil.stmt -> Cil.stmt -> bool

Whether to put this predecessor block in the worklist. We give the * predecessor and the block whose predecessor we are (and whose data has * changed)