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.