Kernel_ast (frama-c-server.Server.Kernel

module Position : Data.S with type t = Frama_c_kernel.Filepos.t

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

Ast Markers

module type Tag = sig ... end

module Decl : Tag with type t = Frama_c_kernel.Printer_tag.declaration

module Marker : Tag with type t = Frama_c_kernel.Printer_tag.localizable

Ast Markers of Specific Kinds

module Lval : sig ... end

Markers that are l-values.

module Stmt : Data.S with type t = Frama_c_kernel.Cil_types.stmt

Markers that are statements.

module Kinstr : Data.S with type t = Frama_c_kernel.Cil_types.kinstr

Optional markers interpreted as kinstr.

Ast Printer

module PrinterTag : Frama_c_kernel.Printer_tag.S_pp

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

val register_fct_filter : 
  Frama_c_kernel.Cil_types.kernel_function filter_registration

Registers a new filter on functions.

val register_var_filter : Frama_c_kernel.Cil_types.varinfo filter_registration

Registers a new filter on variables.