Frama-C:
Plug-ins:
Libraries:

Frama-C API - Kernel_ast

Ast Data

Represented by a Json record with file, dir, basename, line

Ast Markers

module type Tag = sig ... end

Ast Markers of Specific Kinds

module Lval : sig ... end

Markers that are l-values.

Markers that are statements.

Optional markers interpreted as kinstr.

Ast Printer

Ast Information

module Information : sig ... end

Globals

module Functions : sig ... end
type 'a filter_registration = string -> ?labels:(string * string) -> ?default:bool -> ?enable:(unit -> bool) -> ?add_hook:((unit -> unit) -> unit) -> ('a -> bool) -> unit

Definition of a filter on elements of type 'a with a unique name and a boolean function f: 'a -> bool, allowing the user to show/hide elements for which f is true or false. Optional arguments are:

  • labels defines the labels for the positive and negative versions of the filter. By default, they are "<name> elements" and "non-<name> elements".
  • if default is provided, only elements x for which f x = default are shown by default. Otherwise, all elements are shown by default.
  • if enable is provided, the filter is active only when enable () is true. Otherwise, the filter is always active.
  • if hook is provided, it is used to register a hook to notify the server of filter updates (i.e. when f x has changed for some elements).

Registers a new filter on functions.

Registers a new filter on variables.