package goblint-cil

  1. Overview
  2. Docs
On This Page
  1. Internal
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module GoblintCil.FeatureSource

Extending CIL with external features

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

Sourceval register : t -> unit

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

Sourceval list_registered : unit -> t list

List registered features.

Sourceval registered : string -> bool

Check if a given feature is registered.

Sourceval find : string -> t

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

Sourceval enable : string -> unit

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

Sourceval enabled : string -> bool

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

Internal

Sourceval init : unit -> unit

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

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

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

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

OCaml

Innovation. Community. Security.