Frama-C API - extensible_printer_type
The class type that a printer must implement.
Useful functions for building pretty-printers
Local logical annotation (function specifications and code annotations are printed only if logic_printer_enabled
is set to true
.
more info is displayed when on verbose mode. This flag is synchronized with Frama-C's kernel being on debug mode.
method private current_function : Frama_c_kernel.Cil_types.varinfo option
method private current_behavior : Frama_c_kernel.Cil_types.funbehavior option
method private stmt_has_annot : Frama_c_kernel.Cil_types.stmt -> bool
true
if the given statement 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).
method private current_stmt : Frama_c_kernel.Cil_types.stmt option
method private may_be_skipped : Frama_c_kernel.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 -> Frama_c_kernel.Cil_types.block -> bool
method private inline_block : block_ctxt -> Frama_c_kernel.Cil_types.block -> bool
What terminator to print after an instruction. sometimes we want to print sequences of instructions separated by comma
method private opt_funspec : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.funspec -> unit
Pretty-printing of C code
method location : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.location -> unit
method constant : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.constant -> 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 -> Frama_c_kernel.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 -> Frama_c_kernel.Cil_types.varinfo -> unit
Invoked on each variable use.
method lval : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.lval -> unit
Invoked on each lvalue occurrence
method field : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.fieldinfo -> unit
method offset : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.offset -> unit
Invoked on each offset occurrence. The second argument is the base.
method typeref : 'a. Frama_c_kernel.Cil_types.typ -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a -> unit
method typedef : 'a. Frama_c_kernel.Cil_types.global -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a -> unit
method global : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.global -> unit
Global (vars, types, etc.). This can be slow.
method fieldinfo : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.fieldinfo -> unit
A field declaration
method storage : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.storage -> unit
method ikind : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.ikind -> unit
method fkind : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.fkind -> unit
method compkind : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.compinfo -> unit
method compname : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.compinfo -> unit
method compinfo : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.compinfo -> unit
method enumname : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.enuminfo -> unit
method typename : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.typeinfo -> unit
method typ : ?fundecl:Frama_c_kernel.Cil_types.varinfo -> (Stdlib.Format.formatter -> unit) option -> Stdlib.Format.formatter -> Frama_c_kernel.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 -> Frama_c_kernel.Cil_types.attrparam -> unit
Attribute parameter
method attribute : Stdlib.Format.formatter -> Frama_c_kernel.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 -> Frama_c_kernel.Cil_types.attributes -> unit
Attribute lists
method label : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.label -> unit
method compinfo : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.compinfo -> unit
method initinfo : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.initinfo -> unit
method fundec : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.fundec -> unit
method line_directive : ?forcefile:bool -> Stdlib.Format.formatter -> Frama_c_kernel.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 -> Frama_c_kernel.Cil_types.stmt -> unit
Print only the labels of the statement. Used by annotated_stmt
.
method annotated_stmt : Frama_c_kernel.Cil_types.stmt -> Stdlib.Format.formatter -> Frama_c_kernel.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 : Frama_c_kernel.Cil_types.attributes -> Frama_c_kernel.Cil_types.stmt -> Stdlib.Format.formatter -> Frama_c_kernel.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; Printer.extensible_printer
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 -> Frama_c_kernel.Cil_types.instr -> unit
Invoked on each instruction occurrence.
method stmt : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.stmt -> unit
Control-flow statement. annot
is true
iff the printer prints the annotations of the stmt.
method next_stmt : Frama_c_kernel.Cil_types.stmt -> Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.stmt -> unit
method block : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.block -> unit
Prints a block.
method exp : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.exp -> unit
Print expressions
method unop : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.unop -> unit
method binop : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.binop -> unit
method init : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.init -> unit
method file : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.file -> unit
Print initializers. This can be slow.
Pretty-printing of annotations
method logic_constant : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.logic_constant -> unit
method logic_type : (Stdlib.Format.formatter -> unit) option -> Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.logic_type -> unit
method logic_type_def : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.logic_type_def -> unit
method model_info : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.model_info -> unit
method term_binop : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.binop -> unit
method relation : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.relation -> unit
method identified_term : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.identified_term -> unit
method term : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.term -> unit
method term_node : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.term -> unit
method term_lval : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.term_lval -> unit
method term_lhost : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.term_lhost -> unit
method model_field : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.model_info -> unit
method term_offset : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.term_offset -> unit
method logic_builtin_label : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.logic_builtin_label -> unit
method logic_label : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.logic_label -> unit
method logic_info : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.logic_info -> unit
method builtin_logic_info : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.builtin_logic_info -> unit
method logic_type_info : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.logic_type_info -> unit
method logic_ctor_info : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.logic_ctor_info -> unit
method logic_var : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.logic_var -> unit
logic names, with full module path if needed (eg. "foo::bar::jazz") Defaults to self#varname
, with the full name truncated to the currently opened module, if any.
method quantifiers : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.quantifiers -> unit
method predicate_node : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.predicate_node -> unit
method predicate : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.predicate -> unit
method identified_predicate : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.identified_predicate -> unit
method behavior : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.funbehavior -> unit
method requires : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.identified_predicate -> unit
method terminates : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.identified_predicate -> unit
method post_cond : Stdlib.Format.formatter -> (Frama_c_kernel.Cil_types.termination_kind * Frama_c_kernel.Cil_types.identified_predicate) -> unit
pretty prints a post condition according to the exit kind it represents
method assumes : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.identified_predicate -> unit
method extended : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.acsl_extension -> unit
method short_extended : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.acsl_extension -> unit
method funspec : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.funspec -> unit
method assigns : string -> Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.assigns -> unit
first parameter is the introducing keyword (e.g. loop_assigns or assigns).
method allocation : isloop:bool -> Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.allocation -> unit
first parameter is the introducing keyword (e.g. loop_allocates, loop_frees, allocates or free)
method from : string -> Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.from -> unit
prints an assignment with its dependencies.
method code_annotation : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.code_annotation -> unit
method global_annotation : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.global_annotation -> unit
method decreases : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.variant -> unit
method variant : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.variant -> unit
Modifying pretty-printer behavior
method pp_while_head : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.exp -> unit
Prints the recovered while (cond)
exit condition of a loop. Note: this method will be called in a context where 'current_stmt' is tied to the original AST conditional statement that exits the loop, as expected.
All C99 keywords except types "char", "int", "long", "signed", "short", "unsigned", "void" and "_XXX" (like "_Bool") *
All ACSL keywords except logic types
method pp_open_annotation : ?block:bool -> ?pre:Frama_c_kernel.Pretty_utils.sformat -> Stdlib.Format.formatter -> unit
method pp_close_annotation : ?block:bool -> ?suf:Frama_c_kernel.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. *