package goblint-cil

  1. Overview
  2. Docs
On This Page
  1. Internal
package goblint-cil
Legend:
Library
Module
Module type
Parameter
Class
Class type

Extending CIL with external features

type t = {
  1. mutable fd_enabled : bool;
    (*

    The enable flag. Set to default value

    *)
  2. fd_name : string;
    (*

    This is used to construct an option "--doxxx" and "--dontxxx" that enable and disable the feature

    *)
  3. fd_description : string;
    (*

    A longer name that can be used to document the new options

    *)
  4. 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.

    *)
  5. fd_doit : Cil.file -> unit;
    (*

    This performs the transformation

    *)
  6. 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

Register a feature to be used by CIL. Feature name must be unique.

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.