Class type Printer_api.extensible_printer_type

class type extensible_printer_type = object .. end

The class type that a printer must implement.

Useful functions for building pretty-printers

val mutable logic_printer_enabled : bool

Local logical annotation (function specifications and code annotations are printed only if logic_printer_enabled is set to true.

val mutable force_brace : bool

If set to true (default is false, some additional braces are printed.

val mutable verbose : bool

more info is displayed when on verbose mode. This flag is synchronized with Frama-C's kernel being on debug mode.

val mutable is_ghost : bool

are we printing ghost code?

method reset : unit -> unit

method private current_function : Cil_types.varinfo option

Returns the varinfo corresponding to the function being printed

method private current_behavior : Cil_types.funbehavior option

Returns the funbehavior being pretty-printed.

method private stmt_has_annot : Cil_types.stmt -> bool

true if the given statement has some annotations attached to it.

Since Phosphorus-20170501-beta1

method private has_annot : bool

true if current_stmt has some annotations attached to it.

method private in_ghost_if_needed : Stdlib.Format.formatter ->
       bool ->
       ?break_ghost:bool ->
       post_fmt:((Stdlib.Format.formatter -> unit) -> unit, Stdlib.Format.formatter,
                 unit)
                Stdlib.format ->
       ?block:bool -> (unit -> unit) -> unit

Open a ghost context if the the first 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).

Since 20.0-Calcium

method private current_stmt : Cil_types.stmt option

Returns the stmt being printed

method private may_be_skipped : Cil_types.stmt -> bool

This is called to check that a given statement may be compacted with another one. For example this is called whenever a 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

Returns true if the given block must be enclosed in a pair of braces, given the context in which it appears.

Change in Fluorine-20130401

Change in Phosphorus-20170501-beta1

method private inline_block : block_ctxt -> Cil_types.block -> bool

Returns 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).

Change in Fluorine-20130401

Change in Phosphorus-20170501-beta1

method private get_instr_terminator : unit -> string

What terminator to print after an instruction. sometimes we want to print sequences of instructions separated by comma

method private set_instr_terminator : string -> unit

method private opt_funspec : Stdlib.Format.formatter -> Cil_types.funspec -> unit

Pretty-printing of C code

method location : Stdlib.Format.formatter -> Cil_types.location -> unit

method constant : Stdlib.Format.formatter -> Cil_types.constant -> unit

method varname : Stdlib.Format.formatter -> string -> unit

Invoked each time an identifier name is to be printed. Allows for various manipulation of the name, such as unmangling.

method vdecl : Stdlib.Format.formatter -> Cil_types.varinfo -> unit

Invoked for each variable declaration. Note that variable declarations are all the GVar, GVarDecl, GFun, GFunDecl, all the varinfo in formals of function types, and the formals and locals for function definitions.

method varinfo : Stdlib.Format.formatter -> Cil_types.varinfo -> unit

Invoked on each variable use.

method lval : Stdlib.Format.formatter -> Cil_types.lval -> unit

Invoked on each lvalue occurrence

method field : Stdlib.Format.formatter -> Cil_types.fieldinfo -> unit

method offset : Stdlib.Format.formatter -> Cil_types.offset -> unit

Invoked on each offset occurrence. The second argument is the base.

method global : Stdlib.Format.formatter -> Cil_types.global -> unit

Global (vars, types, etc.). This can be slow.

method fieldinfo : Stdlib.Format.formatter -> Cil_types.fieldinfo -> unit

A field declaration

method storage : Stdlib.Format.formatter -> Cil_types.storage -> unit

method ikind : Stdlib.Format.formatter -> Cil_types.ikind -> unit

method fkind : Stdlib.Format.formatter -> Cil_types.fkind -> unit

method typ : ?fundecl:Cil_types.varinfo ->
       (Stdlib.Format.formatter -> unit) option ->
       Stdlib.Format.formatter -> Cil_types.typ -> unit

Use of some type in some declaration. 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 : Stdlib.Format.formatter -> Cil_types.attrparam -> unit

Attribute parameter

method attribute : Stdlib.Format.formatter -> Cil_types.attribute -> bool

Attribute. Also return an indication whether this attribute must be printed inside the __attribute__ list or not.

method attributes : Stdlib.Format.formatter -> Cil_types.attributes -> unit

Attribute lists

method label : Stdlib.Format.formatter -> Cil_types.label -> unit

method compinfo : Stdlib.Format.formatter -> Cil_types.compinfo -> unit

method initinfo : Stdlib.Format.formatter -> Cil_types.initinfo -> unit

method fundec : Stdlib.Format.formatter -> Cil_types.fundec -> unit

method line_directive : ?forcefile:bool -> Stdlib.Format.formatter -> Cil_types.location -> unit

Print a line-number. This is assumed to come always on an empty line. If the forcefile argument is present and is true then the file name will be printed always. Otherwise the file name is printed only if it is different from the last time this function is called. The last file name is stored in a private field inside the cilPrinter object.

method stmt_labels : Stdlib.Format.formatter -> Cil_types.stmt -> unit

Print only the labels of the statement. Used by annotated_stmt.

method annotated_stmt : Cil_types.stmt -> Stdlib.Format.formatter -> Cil_types.stmt -> unit

Print an annotated statement. The code to be printed is given in the last 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 -> Stdlib.Format.formatter -> Cil_types.stmtkind -> unit

Print a statement kind. The code to be printed is given in the 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 : Stdlib.Format.formatter -> Cil_types.instr -> unit

Invoked on each instruction occurrence.

method stmt : Stdlib.Format.formatter -> Cil_types.stmt -> unit

Control-flow statement. annot is true iff the printer prints the annotations of the stmt.

method next_stmt : Cil_types.stmt -> Stdlib.Format.formatter -> Cil_types.stmt -> unit

method block : Stdlib.Format.formatter -> Cil_types.block -> unit

Prints a block.

Change in Fluorine-20130401

Change in Phosphorus-20170501-beta1

method exp : Stdlib.Format.formatter -> Cil_types.exp -> unit

Print expressions

method unop : Stdlib.Format.formatter -> Cil_types.unop -> unit

method binop : Stdlib.Format.formatter -> Cil_types.binop -> unit

method init : Stdlib.Format.formatter -> Cil_types.init -> unit

method file : Stdlib.Format.formatter -> Cil_types.file -> unit

Print initializers. This can be slow.

Pretty-printing of annotations

method logic_constant : Stdlib.Format.formatter -> Cil_types.logic_constant -> unit

method logic_type : (Stdlib.Format.formatter -> unit) option ->
       Stdlib.Format.formatter -> Cil_types.logic_type -> unit

method logic_type_def : Stdlib.Format.formatter -> Cil_types.logic_type_def -> unit

method model_info : Stdlib.Format.formatter -> Cil_types.model_info -> unit

method term_binop : Stdlib.Format.formatter -> Cil_types.binop -> unit

method relation : Stdlib.Format.formatter -> Cil_types.relation -> unit

method identified_term : Stdlib.Format.formatter -> Cil_types.identified_term -> unit

method term : Stdlib.Format.formatter -> Cil_types.term -> unit

method term_node : Stdlib.Format.formatter -> Cil_types.term -> unit

method term_lval : Stdlib.Format.formatter -> Cil_types.term_lval -> unit

method term_lhost : Stdlib.Format.formatter -> Cil_types.term_lhost -> unit

method model_field : Stdlib.Format.formatter -> Cil_types.model_info -> unit

method term_offset : Stdlib.Format.formatter -> Cil_types.term_offset -> unit

method logic_builtin_label : Stdlib.Format.formatter -> Cil_types.logic_builtin_label -> unit

method logic_label : Stdlib.Format.formatter -> Cil_types.logic_label -> unit

method logic_info : Stdlib.Format.formatter -> Cil_types.logic_info -> unit

method builtin_logic_info : Stdlib.Format.formatter -> Cil_types.builtin_logic_info -> unit

method logic_type_info : Stdlib.Format.formatter -> Cil_types.logic_type_info -> unit

method logic_ctor_info : Stdlib.Format.formatter -> Cil_types.logic_ctor_info -> unit

method logic_var : Stdlib.Format.formatter -> Cil_types.logic_var -> unit

method quantifiers : Stdlib.Format.formatter -> Cil_types.quantifiers -> unit

method predicate_node : Stdlib.Format.formatter -> Cil_types.predicate_node -> unit

method predicate : Stdlib.Format.formatter -> Cil_types.predicate -> unit

method identified_predicate : Stdlib.Format.formatter -> Cil_types.identified_predicate -> unit

method behavior : Stdlib.Format.formatter -> Cil_types.funbehavior -> unit

method requires : Stdlib.Format.formatter -> Cil_types.identified_predicate -> unit

method complete_behaviors : Stdlib.Format.formatter -> string list -> unit

method disjoint_behaviors : Stdlib.Format.formatter -> string list -> unit

method terminates : Stdlib.Format.formatter -> Cil_types.identified_predicate -> unit

method post_cond : Stdlib.Format.formatter ->
       Cil_types.termination_kind * Cil_types.identified_predicate -> unit

pretty prints a post condition according to the exit kind it represents

Change in Boron-20100401

pEnsures

method assumes : Stdlib.Format.formatter -> Cil_types.identified_predicate -> unit

method extended : Stdlib.Format.formatter -> Cil_types.acsl_extension -> unit

method short_extended : Stdlib.Format.formatter -> Cil_types.acsl_extension -> unit

method funspec : Stdlib.Format.formatter -> Cil_types.funspec -> unit

method assigns : string -> Stdlib.Format.formatter -> Cil_types.assigns -> unit

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

method allocation : isloop:bool -> Stdlib.Format.formatter -> Cil_types.allocation -> unit

first parameter is the introducing keyword (e.g. loop_allocates, loop_frees, allocates or free)

Since Oxygen-20120901.

method from : string -> Stdlib.Format.formatter -> Cil_types.from -> unit

prints an assignment with its dependencies.

method code_annotation : Stdlib.Format.formatter -> Cil_types.code_annotation -> unit

method global_annotation : Stdlib.Format.formatter -> Cil_types.global_annotation -> unit

method decreases : Stdlib.Format.formatter -> Cil_types.variant -> unit

method variant : Stdlib.Format.formatter -> Cil_types.variant -> unit

method pp_keyword : Stdlib.Format.formatter -> string -> unit

Modifying pretty-printer behavior

All C99 keywords except types "char", "int", "long", "signed", "short", "unsigned", "void" and "_XXX" (like "_Bool") *

method pp_acsl_keyword : Stdlib.Format.formatter -> string -> unit

All ACSL keywords except logic types

method pp_open_annotation : ?block:bool -> ?pre:Pretty_utils.sformat -> Stdlib.Format.formatter -> unit

method pp_close_annotation : ?block:bool -> ?suf:Pretty_utils.sformat -> Stdlib.Format.formatter -> unit

Called before/after printing an annotation comment. Put the annotation in a block according to the optional argument. If it is not set, the annotation is put in a block. *

method without_annot : 'a.
         (Stdlib.Format.formatter -> 'a -> unit) ->
         Stdlib.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.
         (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.