package goblint-cil

You can search for identifiers within the package.

in-package search v0.2.0

package goblint-cil

goblint-cil
- Alpha
- Bitmap
- Cabs
- Cabs2cil
- Cabshelper
- Cabsvisit
  - cabsVisitor
  - nopCabsVisitor
- Cfg
- Check
- Cil
- Cilint
- Cillower
- Ciloptions
- Ciltools
- Cilutil
- Cilversion
- Clexer
- Clist
- Cparser
- Cprint
- Dataflow
- Dominators
- Errormsg
- Escape
- Expcompare
  - volatileFinderClass
- Feature
- Formatcil
- Formatlex
- Formatparse
- Frontc
- GrowArray
- Inthash
- Lexerhack
- Libmaincil
  - unrollVisitorClass
- Longarray
- Machdep
- Machdepenv
- Mergecil
- Patch
- Pretty
  - MakeMapPrinter
    
    Map
  - MakeSetPrinter
    
    Set
- Rmtmps
- Stats
- Trace
- Util
- Whitetrack
goblint-cil.dataslicing
- Dataslicing
goblint-cil.liveness
- Liveness
- Usedef
  - VS
  - useDefVisitorClass
goblint-cil.makecfg
- MakeCFG
  - callBBVisitor
  - vidVisitor
goblint-cil.pta
- Golf
- Olf
- Ptranal
- Setp
  - Make
    
    Ord
  - PolyOrderedType
  - S
- Steensgaard
- Uref
goblint-cil.syntacticsearch
goblint-cil.zrapp

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.