package goblint-cil

  1. Overview
  2. Docs
package goblint-cil
Legend:
Library
Module
Module type
Parameter
Class
Class type
val name : string

For debugging purposes, the name of the analysis

val debug : bool 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 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 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 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.