Frama-C API - extensible_printer

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

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

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

are we printing ghost code?

• returns

  the varinfo corresponding to the function being printed

• returns

  the funbehavior being pretty-printed.

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

• since Phosphorus-20170501-beta1

true if current_stmt has some annotations attached to it.

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

• returns

  the stmt being printed

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

• returns

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

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

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

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

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.

Invoked on each variable use.

Invoked on each lvalue occurrence

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

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

A field declaration

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.

Attribute parameter

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

Attribute lists

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.

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

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.

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)

Invoked on each instruction occurrence.

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

Prints a block.

Print expressions

Print initializers. This can be slow.

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.

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

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

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

• since Oxygen-20120901.

prints an assignment with its dependencies.

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

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. *

self#without_annot printer fmt x pretty prints x by using printer, without pretty-printing its function contracts and code annotations.

self#force_brace printer fmt x pretty prints x by using printer, but add some extra braces '{' and '}' which are hidden by default.