package goblint-cil

You can search for identifiers within the package.

in-package search v0.2.0

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

A framework for data flow analysis for CIL code. Before using this framework, you must initialize the Control-flow Graph for your program, e.g using Cfg.computeFileCFG

type 't action =

| Default
(*
The default action
*)
| Done of 't
(*
Do not do the default action. Use this result
*)
| Post of 't -> 't
(*
The default action, followed by the given * transformer
*)

type 't stmtaction =

| SDefault
(*
The default action
*)
| SDone
(*
Do not visit this statement or its successors
*)
| SUse of 't
(*
Visit the instructions and successors of this statement as usual, but use the specified state instead of the one that was passed to doStmt
*)

type 't guardaction =

| GDefault
(*
The default state
*)
| GUse of 't
(*
Use this data for the branch
*)
| GUnreachable
(*
The branch will never be taken.
*)

module type ForwardsTransfer = sig ... end

module ForwardsDataFlow (T : ForwardsTransfer) : sig ... end

module type BackwardsTransfer = sig ... end

module BackwardsDataFlow (T : BackwardsTransfer) : sig ... end

val find_stmts : Cil.fundec -> Cil.stmt list * Cil.stmt list

Returns (all_stmts, sink_stmts), where all_stmts is a list of the statements in a function, and sink_stmts is a list of the return statments (including statements that fall through the end of a void function). Useful when you need an initial set of statements for BackwardsDataFlow.compute.