package goblint-cil

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Internal

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

Extending CIL with external features

type t = {

mutable fd_enabled : bool;
(*
The enable flag. Set to default value
*)
fd_name : string;
(*
This is used to construct an option "--doxxx" and "--dontxxx" that enable and disable the feature
*)
fd_description : string;
(*
A longer name that can be used to document the new options
*)
fd_extraopt : (string * Arg.spec * string) list;
(*
Additional command line options. The description strings should usually start with a space for Arg.align to print the --help nicely.
*)
fd_doit : Cil.file -> unit;
(*
This performs the transformation
*)
fd_post_check : bool;
(*
Whether to perform a CIL consistency checking after this stage, if checking is enabled (--check is passed to cilly). Set this to true if your feature makes any changes for the program.
*)

}

Description of a CIL feature.

val register : t -> unit

val list_registered : unit -> t list

List registered features.

val registered : string -> bool

Check if a given feature is registered.

val find : string -> t

Find a feature by name. Raise Not_found if the feature is not registered.

val enable : string -> unit

Enable a given feature, by name. Raise Errormsg.Error if the feature is not registered.

val enabled : string -> bool

Check if a given feature is enabled. Return false if the feature is not registered.

Internal

val init : unit -> unit

Initialize the module. This needs to be called before loadWithDeps is used. Called automatically by loadFromArgv.

val loadWithDeps : string -> unit

Find and dynamically links a module. The name should be either a path to a cmo, cma or cmxs file, or the name of a findlib package. In the latter case, package dependencies are loaded automatically. Each file is loaded at most one. The loaded module must call register to make its features available to CIL.

val loadFromArgv : string -> unit

loadFromArgv switch searches Sys.argv for the command-line option switch, and loads the modules passed as parameters. Ignores every other Sys.argv element.

val loadFromEnv : string -> string list -> unit

loadFromEnv name default loads coma-separated module names stored in the environment variable name, or default if it is not defined.