package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Internal Cil printer.

Must not be used by plug-in developers: use module Printer instead. In particular, this pretty-printer is incorrect regarding annotations. It should only be used by modules linked before Annotations.

  • since Fluorine-20130401
include Printer_api.S
include Printer_api.S_pp
val pp_varname : Stdlib.Format.formatter -> string -> unit

Printer for C constructs

val pp_location : Stdlib.Format.formatter -> Cil_types.location -> unit
val pp_constant : Stdlib.Format.formatter -> Cil_types.constant -> unit
val pp_storage : Stdlib.Format.formatter -> Cil_types.storage -> unit
val pp_ikind : Stdlib.Format.formatter -> Cil_types.ikind -> unit
val pp_fkind : Stdlib.Format.formatter -> Cil_types.fkind -> unit
val pp_typ : Stdlib.Format.formatter -> Cil_types.typ -> unit
val pp_exp : Stdlib.Format.formatter -> Cil_types.exp -> unit
val pp_vdecl : Stdlib.Format.formatter -> Cil_types.varinfo -> unit
val pp_varinfo : Stdlib.Format.formatter -> Cil_types.varinfo -> unit
val pp_lval : Stdlib.Format.formatter -> Cil_types.lval -> unit
val pp_field : Stdlib.Format.formatter -> Cil_types.fieldinfo -> unit
val pp_offset : Stdlib.Format.formatter -> Cil_types.offset -> unit
val pp_init : Stdlib.Format.formatter -> Cil_types.init -> unit
val pp_binop : Stdlib.Format.formatter -> Cil_types.binop -> unit
val pp_unop : Stdlib.Format.formatter -> Cil_types.unop -> unit
val pp_attribute : Stdlib.Format.formatter -> Cil_types.attribute -> unit
val pp_attrparam : Stdlib.Format.formatter -> Cil_types.attrparam -> unit
val pp_attributes : Stdlib.Format.formatter -> Cil_types.attributes -> unit
val pp_instr : Stdlib.Format.formatter -> Cil_types.instr -> unit
val pp_label : Stdlib.Format.formatter -> Cil_types.label -> unit
val pp_stmt : Stdlib.Format.formatter -> Cil_types.stmt -> unit
val pp_block : Stdlib.Format.formatter -> Cil_types.block -> unit
val pp_global : Stdlib.Format.formatter -> Cil_types.global -> unit
val pp_file : Stdlib.Format.formatter -> Cil_types.file -> unit
val pp_compinfo : Stdlib.Format.formatter -> Cil_types.compinfo -> unit
val pp_logic_type_info : Stdlib.Format.formatter -> Cil_types.logic_type_info -> unit
val pp_logic_ctor_info : Stdlib.Format.formatter -> Cil_types.logic_ctor_info -> unit
val pp_initinfo : Stdlib.Format.formatter -> Cil_types.initinfo -> unit
val pp_logic_info : Stdlib.Format.formatter -> Cil_types.logic_info -> unit
val pp_logic_constant : Stdlib.Format.formatter -> Cil_types.logic_constant -> unit
val pp_fundec : Stdlib.Format.formatter -> Cil_types.fundec -> unit

Printer for ACSL constructs

val pp_relation : Stdlib.Format.formatter -> Cil_types.relation -> unit
val pp_model_info : Stdlib.Format.formatter -> Cil_types.model_info -> unit
  • since Oxygen-20120901
val pp_term_lval : Stdlib.Format.formatter -> Cil_types.term_lval -> unit
val pp_term_lhost : Stdlib.Format.formatter -> Cil_types.term_lhost -> unit
val pp_logic_var : Stdlib.Format.formatter -> Cil_types.logic_var -> unit
val pp_logic_type : Stdlib.Format.formatter -> Cil_types.logic_type -> unit
val pp_identified_term : Stdlib.Format.formatter -> Cil_types.identified_term -> unit
val pp_term : Stdlib.Format.formatter -> Cil_types.term -> unit
val pp_model_field : Stdlib.Format.formatter -> Cil_types.model_info -> unit
val pp_term_offset : Stdlib.Format.formatter -> Cil_types.term_offset -> unit
val pp_logic_builtin_label : Stdlib.Format.formatter -> Cil_types.logic_builtin_label -> unit
val pp_logic_label : Stdlib.Format.formatter -> Cil_types.logic_label -> unit
val pp_builtin_logic_info : Stdlib.Format.formatter -> Cil_types.builtin_logic_info -> unit
val pp_extended : Stdlib.Format.formatter -> Cil_types.acsl_extension -> unit
val pp_short_extended : Stdlib.Format.formatter -> Cil_types.acsl_extension -> unit
  • since 21.0-Scandium
val pp_predicate_node : Stdlib.Format.formatter -> Cil_types.predicate_node -> unit
val pp_predicate : Stdlib.Format.formatter -> Cil_types.predicate -> unit
val pp_toplevel_predicate : Stdlib.Format.formatter -> Cil_types.toplevel_predicate -> unit
  • since 22.0-Titanium
val pp_identified_predicate : Stdlib.Format.formatter -> Cil_types.identified_predicate -> unit
val pp_code_annotation : Stdlib.Format.formatter -> Cil_types.code_annotation -> unit
val pp_funspec : Stdlib.Format.formatter -> Cil_types.funspec -> unit
val pp_behavior : Stdlib.Format.formatter -> Cil_types.funbehavior -> unit
val pp_global_annotation : Stdlib.Format.formatter -> Cil_types.global_annotation -> unit
val pp_decreases : Stdlib.Format.formatter -> Cil_types.variant -> unit
val pp_variant : Stdlib.Format.formatter -> Cil_types.variant -> unit
val pp_from : Stdlib.Format.formatter -> Cil_types.from -> unit
val pp_assigns : Stdlib.Format.formatter -> Cil_types.assigns -> unit
val pp_allocation : Stdlib.Format.formatter -> Cil_types.allocation -> unit
  • since Oxygen-20120901
val pp_loop_from : Stdlib.Format.formatter -> Cil_types.from -> unit
val pp_loop_assigns : Stdlib.Format.formatter -> Cil_types.assigns -> unit
val pp_loop_allocation : Stdlib.Format.formatter -> Cil_types.allocation -> unit
  • since Oxygen-20120901
val pp_post_cond : Stdlib.Format.formatter -> (Cil_types.termination_kind * Cil_types.identified_predicate) -> unit

General form of printers

val pp_full_assigns : string -> Stdlib.Format.formatter -> Cil_types.assigns -> unit

first parameter is the introducing keyword (e.g. loop_assigns or assigns).

val without_annot : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a -> unit

without_annot printer fmt x pretty prints x by using printer, without pretty-printing its function contracts and code annotations.

val force_brace : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a -> unit

self#force_brace printer fmt x pretty prints x by using printer, but add some extra braces '{' and '}' which are hidden by default.

Extensible printer

Extend this class if you want to obtain a custom pretty-printer.

module type PrinterClass = sig ... end

Auxiliary module type for a pretty-printer

module type PrinterExtension = functor (X : PrinterClass) -> PrinterClass

Signature for extending an existing pretty-printer. OCaml forbids inheriting from a class received as argument, so we use a functor instead.

val update_printer : (module PrinterExtension) -> unit

Register a pretty-printer extension. The pretty-printer passed as argument X in the functor PrinterExtension is the current pretty-printer, which you should inherit from.

This is how this function should be used:

module PrinterClassDeferred (X: Printer.PrinterClass) = struct
  class printer : Printer.extensible_printer = object(self)
    inherit X.printer as super
    (* Override the standard methods *)
  end
end
let () = Printer.update_printer
    (module PrinterClassDeferred: Printer.PrinterExtension)
val current_printer : unit -> (module PrinterClass)

Returns the current pretty-printer, with all the extensions added using update_printer.

val set_printer : (module PrinterClass) -> unit

Set the current pretty-printer, typically to a printer previously obtained through current_printer. This can be useful to cancel a modification performed through update_printer.

val string_of_assert : Cil_types.predicate_kind -> string

"assert", "check" or "admit".

val name_of_assert : Cil_types.predicate_kind -> string

"assertion", "check" or "admit".

val string_of_lemma : Cil_types.predicate_kind -> string

"lemma", "check lemma" or "axiom".

val string_of_predicate : kw:string -> Cil_types.predicate_kind -> string

clause, prefixed by "check" or "admit".

val ident_of_lemma : Cil_types.predicate_kind -> string

same as string_of_lemma with "_" for separator.

val ident_of_predicate : kw:string -> Cil_types.predicate_kind -> string

same as string_of_predicate with "_" for separator.

val pp_assert_kind : Stdlib.Format.formatter -> Cil_types.predicate_kind -> unit

pretty prints string_of_assert.

val pp_lemma_kind : Stdlib.Format.formatter -> Cil_types.predicate_kind -> unit

pretty prints string_of_lemma.

val pp_predicate_kind : kw:string -> Stdlib.Format.formatter -> Cil_types.predicate_kind -> unit

pretty prints string_of_predicate.

val get_termination_kind_name : Cil_types.termination_kind -> string
val register_shallow_attribute : string -> unit

Register an attribute that will never be pretty printed.

val state : Printer_api.state
val print_global : Cil_types.global -> bool

Is the given global displayed by the pretty-printer.

  • since Aluminium-20160501
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct