Module Frama_c_kernel.Logic_print

Pretty-printing of a parsed logic tree.

val print_constant : Format.formatter -> Logic_ptree.constant -> unit
val print_logic_type : (Format.formatter -> unit) option -> Format.formatter -> Logic_ptree.logic_type -> unit

First arguments prints the name of identifier declared with the corresponding type (None for pure type. C syntax makes impossible to separate printing the type and the identifier in a declaration...

val print_quantifiers : Format.formatter -> Logic_ptree.quantifiers -> unit
val print_lexpr : Format.formatter -> Logic_ptree.lexpr -> unit
val print_type_annot : Format.formatter -> Logic_ptree.type_annot -> unit
val print_typedef : Format.formatter -> Logic_ptree.typedef -> unit
val print_decl : Format.formatter -> Logic_ptree.decl -> unit
val print_spec : Format.formatter -> Logic_ptree.spec -> unit
val print_code_annot : Format.formatter -> Logic_ptree.code_annot -> unit
val print_assigns : Format.formatter -> Logic_ptree.assigns -> unit
val print_variant : Format.formatter -> Logic_ptree.variant -> unit