package goblint-cil

You can search for identifiers within the package.

in-package search v0.2.0

package goblint-cil

goblint-cil
- GoblintCil
  - Alpha
  - Cabs
  - Cabs2cil
  - Cabshelper
  - Cabsvisit
    
    cabsVisitor
    
    nopCabsVisitor
  - Cfg
  - Check
  - Cil
    
    cilPrinter
    
    cilVisitor
    
    defaultCilPrinterClass
    
    descriptiveCilPrinter
    
    descriptiveCilPrinterClass
    
    nopCilVisitor
    
    plainCilPrinterClass
  - Cilint
  - Cillower
  - Ciltools
    
    attribute_checker
    
    callBBVisitor
    
    sidVisitor
    
    vidVisitor
  - Cilutil
  - Cprint
  - Dataflow
    
    BackwardsDataFlow
    
    T
    
    BackwardsTransfer
    
    ForwardsDataFlow
    
    T
    
    ForwardsTransfer
  - Dominators
  - Errormsg
  - Escape
  - Expcompare
    
    volatileFinderClass
  - Feature
  - Formatcil
  - Frontc
  - GrowArray
  - Inthash
  - Machdep
  - Machdepenv
  - Mergecil
  - Patch
  - Pretty
    
    MakeMapPrinter
    
    Map
    
    MakeSetPrinter
    
    Set
  - RmUnused
  - Stats
  - Trace
  - Util
  - Whitetrack
  - cilPrinter
  - cilVisitor
  - defaultCilPrinterClass
  - descriptiveCilPrinter
  - descriptiveCilPrinterClass
  - nopCilVisitor
  - plainCilPrinterClass
goblint-cil.dataslicing
- Dataslicing
goblint-cil.liveness
- Liveness
goblint-cil.makecfg
- Makecfg
  - MakeCFG
    
    callBBVisitor
    
    vidVisitor
goblint-cil.pta
- Ptranal
goblint-cil.syntacticsearch
- Syntacticsearch
goblint-cil.zrapp
- Zrapp
  - zraCilPrinterClass

Legend:
Library
Module
Module type
Parameter
Class
Class type

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. 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.

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

Pretty-print the state

val 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

val 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.

val 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.

val combineSuccessors : t -> t -> t

Take the data from two successors and combine it

val 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)

val 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)

val 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)