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