package frama-c
Install
Dune Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
NNicolas Bellec
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
VVincent Botbol
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
TTristan Le Gall
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
JJulien Signoles
-
NNicolas Stouls
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493
doc/frama-c.kernel/Frama_c_kernel/Printer_api/index.html
Module Frama_c_kernel.Printer_api
Type of AST's extensible printers.
type block_ctxt =
| Stmt_block of Cil_types.stmt
(*stmt is Block b.
*)| Body
(*body of a function.
*)| Then_with_else
(*block is the then branch of a conditional that has an else branch.
*)| Other
(*block is any other toplevel block of the cfg (then without else, else branch, switch, while, ...
*)
context in which a block will be printed. useful to decide whether braces are required or not.
Class type for extensible printer
class type extensible_printer_type = object ... end
The class type that a printer must implement.
Types for customizing pretty printers
type line_directive_style =
| Line_comment
(*Before every element, print the line number in comments. This is ignored by processing tools (thus errors are reported on the lines of the CIL output), but useful for visual inspection
*)| Line_comment_sparse
(*Like LineComment but only print a line directive for a new source line
*)| Line_preprocessor_input
(*Use #line directives
*)| Line_preprocessor_output
(*Use # nnn directives (in gcc mode)
*)
Styles of printing line directives
type state = {
mutable line_directive_style : line_directive_style option;
(*How to print line directives
*)mutable print_cil_input : bool;
(*Whether we print something that will only be used as input to Cil's parser. In that case we are a bit more liberal in what we print.
*)mutable print_cil_as_is : bool;
(*Whether to print the CIL as they are, without trying to be smart and print nicer code. Normally this is false, in which case the pretty printer will turn the while(1) loops of CIL into nicer loops, will not print empty "else" blocks, etc. There is one case however in which if you turn this on you will get code that does not compile: if you use varargs the __builtin_va_arg function will be printed in its internal form.
*)mutable line_length : int;
(*The length used when wrapping output lines. Setting this variable to a large integer will prevent wrapping and make #line directives more accurate.
*)mutable warn_truncate : bool;
(*Emit warnings when truncating integer constants (default true)
*)
}
Functions for pretty printing
module type S_pp = sig ... end
module type S = sig ... end