Frama-C:
Plug-ins:
Libraries:

Frama-C API - Printer_tag

Utilities to pretty print source with located Ast elements

type declaration =
  1. | SEnum of Cil_types.enuminfo
  2. | SComp of Cil_types.compinfo
  3. | SType of Cil_types.typeinfo
  4. | SGlobal of Cil_types.varinfo
  5. | SFunction of Cil_types.kernel_function

The kind of AST declarations that can be printed.

val pp_declaration : Stdlib.Format.formatter -> declaration -> unit

Prints a concise label of the declaration.

type localizable =
  1. | PStmt of Cil_types.kernel_function * Cil_types.stmt
    (*

    Full statement (with attributes, annotations, etc.)

    *)
  2. | PStmtStart of Cil_types.kernel_function * Cil_types.stmt
    (*

    Naked statement (only skind, without attributes, annotations, etc.)

    *)
  3. | PLval of Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.lval
    (*

    L-Values

    *)
  4. | PExp of Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.exp
    (*

    Non l-value expressions

    *)
  5. | PTermLval of Cil_types.kernel_function option * Cil_types.kinstr * Property.t * Cil_types.term_lval
    (*

    Term l-values inside properties

    *)
  6. | PVDecl of Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.varinfo
    (*

    Declaration and definition of variables and function. Check the type of the varinfo to distinguish between the various possibilities. If the varinfo is a global or a local, the kernel_function is the one in which the variable is declared. The kinstr argument is given for local variables with an explicit initializer.

    *)
  7. | PGlobal of Cil_types.global
    (*

    Global definitions except global variables and functions.

    *)
  8. | PIP of Property.t
  9. | PType of Cil_types.typ

The kind of object that can be selected in the source viewer.

val pp_signature : Stdlib.Format.formatter -> declaration -> unit

Prints the global declaration of the declaration.

val pp_definition : Stdlib.Format.formatter -> declaration -> unit

Prints the global definition of the declaration.

val pp_localizable : Stdlib.Format.formatter -> localizable -> unit

Prints the signature of the localizable.

val pp_debug : Stdlib.Format.formatter -> localizable -> unit

Debugging.

Declaration of Localizable

Localizable items are always printed under a certain global scope identified by a declaration that can be retrieved from declaration_of_type, declaration_of_global, declaration_of_property and declaration_of_localizable functions below.

Moreover, each declared item can be identified in two different ways: a declaration scope and its own localizable inside this scope. Functions localizable_of_kf, localizable_of_global and localizable_of_declaration can be used to obtain the self-localization of declarations.

Differently, some localizable refers to some global declaration, eg. a variable or a function inside an expression or the compound name of a type. In such a case, functions definition_of_type and definition_of_localizable return the localization of the referenced declaration. It is returned as a localization to the associated declaration, whose scope can be obtained in turn with declaration_of_localizable.

val declaration_of_type : Cil_types.typ -> declaration option
val declaration_of_global : Cil_types.global -> declaration option
val declaration_of_property : Property.t -> declaration option
val declaration_of_localizable : localizable -> declaration option
val definition_of_type : Cil_types.typ -> localizable option
val definition_of_localizable : localizable -> localizable option
val loc_of_declaration : declaration -> Cil_types.location
val name_of_type : Cil_types.typ -> string option
val name_of_global : Cil_types.global -> string option
val name_of_declaration : declaration -> string
val name_of_localizable : localizable -> string option
val signature_of_declaration : declaration -> Cil_types.global
val definition_of_declaration : declaration -> Cil_types.global
val localizable_of_kf : Cil_types.kernel_function -> localizable
val localizable_of_global : Cil_types.global -> localizable
val localizable_of_stmt : Cil_types.stmt -> localizable
val localizable_of_declaration : declaration -> localizable
val kf_of_localizable : localizable -> Cil_types.kernel_function option
val ki_of_localizable : localizable -> Cil_types.kinstr
val varinfo_of_localizable : localizable -> Cil_types.varinfo option
val typ_of_localizable : localizable -> Cil_types.typ option
val loc_of_localizable : localizable -> Cil_types.location

Might return Location.unknown

val loc_to_localizable : ?precise_col:bool -> Filepath.position -> localizable option

return the (hopefully) most precise localizable that contains the given Filepath.position. If precise_col is true, takes the column number into account (possibly a more precise, but costly, result).

  • since 24.0-Chromium
module type Tag = sig ... end
module type S_pp = sig ... end
module Make (_ : Tag) : S_pp