Previous  Up  Next

Module Cil_printer

module Cil_printer: sig .. end

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.

include Printer_api.S
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.