class type extensible_printer_type =object
..end
val mutable logic_printer_enabled : bool
logic_printer_enabled
is set to true
.val mutable force_brace : bool
true
(default is false
, some additional braces are
printed.val mutable verbose : bool
val mutable is_ghost : bool
method reset : unit -> unit
method private current_function : Cil_types.varinfo option
varinfo
corresponding to the function being printedmethod private current_behavior : Cil_types.funbehavior option
funbehavior
being pretty-printed.method private stmt_has_annot : Cil_types.stmt -> bool
true
if the given statement has some annotations attached to it.method private has_annot : bool
true
if current_stmt
has some annotations attached to it.method private in_ghost_if_needed : Format.formatter ->
bool ->
?break_ghost:bool ->
post_fmt:((Format.formatter -> unit) -> unit, Format.formatter, unit)
Pervasives.format ->
?block:bool -> (unit -> unit) -> unit
bool
is true and we are not
already in a ghost context. break_ghost
indicates whether we should
break after the ghost
keyword, defaults to true. post_fmt
is a format
like "%t"
and is used to define the format at the end of the ghost
context. block
indicates whether we should open a C block or not
(defaults to true
). The last parameter is the function to be applied in
the ghost context (generally some AST element).method private current_stmt : Cil_types.stmt option
stmt
being printedmethod private may_be_skipped : Cil_types.stmt -> bool
while(1)
followed by a
conditional if (cond) break;
may be compacted into while (cond)
.method private require_braces : block_ctxt -> Cil_types.block -> bool
true
if the given block must be enclosed in a pair of braces,
given the context in which it appears.method private inline_block : block_ctxt -> Cil_types.block -> bool
true
if the given block may be inlined in a single line.
has_annot
indicates if the stmt corresponding to the block may have
annotations (default is true
).method private get_instr_terminator : unit -> string
method private set_instr_terminator : string -> unit
method private opt_funspec : Format.formatter -> Cil_types.funspec -> unit
method location : Format.formatter -> Cil_types.location -> unit
method constant : Format.formatter -> Cil_types.constant -> unit
method varname : Format.formatter -> string -> unit
method vdecl : Format.formatter -> Cil_types.varinfo -> unit
GVar
, GVarDecl
, GFun
, GFunDecl
, all the varinfo
in formals of function types, and the formals and locals for function
definitions.method varinfo : Format.formatter -> Cil_types.varinfo -> unit
method lval : Format.formatter -> Cil_types.lval -> unit
method field : Format.formatter -> Cil_types.fieldinfo -> unit
method offset : Format.formatter -> Cil_types.offset -> unit
method global : Format.formatter -> Cil_types.global -> unit
method fieldinfo : Format.formatter -> Cil_types.fieldinfo -> unit
method storage : Format.formatter -> Cil_types.storage -> unit
method ikind : Format.formatter -> Cil_types.ikind -> unit
method fkind : Format.formatter -> Cil_types.fkind -> unit
method typ : ?fundecl:Cil_types.varinfo ->
(Format.formatter -> unit) option ->
Format.formatter -> Cil_types.typ -> unit
fundecl
is the name of the
function which is declared with the corresponding type. The second
argument is used to print the declared element, or is None if we are just
printing a type with no name being declared. If fundecl
is not None,
second argument must also have a value.method attrparam : Format.formatter -> Cil_types.attrparam -> unit
method attribute : Format.formatter -> Cil_types.attribute -> bool
method attributes : Format.formatter -> Cil_types.attributes -> unit
method label : Format.formatter -> Cil_types.label -> unit
method compinfo : Format.formatter -> Cil_types.compinfo -> unit
method initinfo : Format.formatter -> Cil_types.initinfo -> unit
method fundec : Format.formatter -> Cil_types.fundec -> unit
method line_directive : ?forcefile:bool -> Format.formatter -> Cil_types.location -> unit
method stmt_labels : Format.formatter -> Cil_types.stmt -> unit
annotated_stmt
.method annotated_stmt : Cil_types.stmt -> Format.formatter -> Cil_types.stmt -> unit
Cil_types.stmt
argument. The initial Cil_types.stmt
argument
records the statement which follows the one being printed.method stmtkind : Cil_types.attributes ->
Cil_types.stmt -> Format.formatter -> Cil_types.stmtkind -> unit
Cil_types.stmtkind
argument. The initial Cil_types.stmt
argument
records the statement which follows the one being printed;
defaultCilPrinterClass
uses this information to prettify statement
printing in certain special cases. The boolean flag indicated whether
the statement has labels (which have already been printed)method instr : Format.formatter -> Cil_types.instr -> unit
method stmt : Format.formatter -> Cil_types.stmt -> unit
annot
is true
iff the printer prints the
annotations of the stmt.method next_stmt : Cil_types.stmt -> Format.formatter -> Cil_types.stmt -> unit
method block : Format.formatter -> Cil_types.block -> unit
method exp : Format.formatter -> Cil_types.exp -> unit
method unop : Format.formatter -> Cil_types.unop -> unit
method binop : Format.formatter -> Cil_types.binop -> unit
method init : Format.formatter -> Cil_types.init -> unit
method file : Format.formatter -> Cil_types.file -> unit
method logic_constant : Format.formatter -> Cil_types.logic_constant -> unit
method logic_type : (Format.formatter -> unit) option ->
Format.formatter -> Cil_types.logic_type -> unit
method logic_type_def : Format.formatter -> Cil_types.logic_type_def -> unit
method model_info : Format.formatter -> Cil_types.model_info -> unit
method term_binop : Format.formatter -> Cil_types.binop -> unit
method relation : Format.formatter -> Cil_types.relation -> unit
method identified_term : Format.formatter -> Cil_types.identified_term -> unit
method term : Format.formatter -> Cil_types.term -> unit
method term_node : Format.formatter -> Cil_types.term -> unit
method term_lval : Format.formatter -> Cil_types.term_lval -> unit
method term_lhost : Format.formatter -> Cil_types.term_lhost -> unit
method model_field : Format.formatter -> Cil_types.model_info -> unit
method term_offset : Format.formatter -> Cil_types.term_offset -> unit
method logic_builtin_label : Format.formatter -> Cil_types.logic_builtin_label -> unit
method logic_label : Format.formatter -> Cil_types.logic_label -> unit
method logic_info : Format.formatter -> Cil_types.logic_info -> unit
method builtin_logic_info : Format.formatter -> Cil_types.builtin_logic_info -> unit
method logic_type_info : Format.formatter -> Cil_types.logic_type_info -> unit
method logic_ctor_info : Format.formatter -> Cil_types.logic_ctor_info -> unit
method logic_var : Format.formatter -> Cil_types.logic_var -> unit
method quantifiers : Format.formatter -> Cil_types.quantifiers -> unit
method predicate_node : Format.formatter -> Cil_types.predicate_node -> unit
method predicate : Format.formatter -> Cil_types.predicate -> unit
method identified_predicate : Format.formatter -> Cil_types.identified_predicate -> unit
method behavior : Format.formatter -> Cil_types.funbehavior -> unit
method requires : Format.formatter -> Cil_types.identified_predicate -> unit
method complete_behaviors : Format.formatter -> string list -> unit
method disjoint_behaviors : Format.formatter -> string list -> unit
method terminates : Format.formatter -> Cil_types.identified_predicate -> unit
method post_cond : Format.formatter ->
Cil_types.termination_kind * Cil_types.identified_predicate -> unit
pEnsures
method assumes : Format.formatter -> Cil_types.identified_predicate -> unit
method extended : Format.formatter -> Cil_types.acsl_extension -> unit
method short_extended : Format.formatter -> Cil_types.acsl_extension -> unit
method funspec : Format.formatter -> Cil_types.funspec -> unit
method assigns : string -> Format.formatter -> Cil_types.assigns -> unit
method allocation : isloop:bool -> Format.formatter -> Cil_types.allocation -> unit
method from : string -> Format.formatter -> Cil_types.from -> unit
method code_annotation : Format.formatter -> Cil_types.code_annotation -> unit
method global_annotation : Format.formatter -> Cil_types.global_annotation -> unit
method decreases : Format.formatter -> Cil_types.variant -> unit
method variant : Format.formatter -> Cil_types.variant -> unit
method pp_keyword : Format.formatter -> string -> unit
All C99 keywords except types "char", "int", "long", "signed",
"short", "unsigned", "void" and "_XXX" (like "_Bool") *
method pp_acsl_keyword : Format.formatter -> string -> unit
method pp_open_annotation : ?block:bool -> ?pre:Pretty_utils.sformat -> Format.formatter -> unit
method pp_close_annotation : ?block:bool -> ?suf:Pretty_utils.sformat -> Format.formatter -> unit
method without_annot : 'a. (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit
self#without_annot printer fmt x
pretty prints x
by using printer
,
without pretty-printing its function contracts and code annotations.method force_brace : 'a. (Format.formatter -> 'a -> unit) -> 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.