Kernel_ast.Printerinclude Frama_c_kernel.Printer_api.S_ppval pp_varname : Format.formatter -> string -> unitval pp_location : Format.formatter -> Frama_c_kernel.Cil_types.location -> unitval pp_constant : Format.formatter -> Frama_c_kernel.Cil_types.constant -> unitval pp_storage : Format.formatter -> Frama_c_kernel.Cil_types.storage -> unitval pp_ikind : Format.formatter -> Frama_c_kernel.Cil_types.ikind -> unitval pp_fkind : Format.formatter -> Frama_c_kernel.Cil_types.fkind -> unitval pp_typ : Format.formatter -> Frama_c_kernel.Cil_types.typ -> unitval pp_exp : Format.formatter -> Frama_c_kernel.Cil_types.exp -> unitval pp_vdecl : Format.formatter -> Frama_c_kernel.Cil_types.varinfo -> unitval pp_varinfo : Format.formatter -> Frama_c_kernel.Cil_types.varinfo -> unitval pp_lval : Format.formatter -> Frama_c_kernel.Cil_types.lval -> unitval pp_field : Format.formatter -> Frama_c_kernel.Cil_types.fieldinfo -> unitval pp_offset : Format.formatter -> Frama_c_kernel.Cil_types.offset -> unitval pp_init : Format.formatter -> Frama_c_kernel.Cil_types.init -> unitval pp_binop : Format.formatter -> Frama_c_kernel.Cil_types.binop -> unitval pp_unop : Format.formatter -> Frama_c_kernel.Cil_types.unop -> unitval pp_attribute :
Format.formatter ->
Frama_c_kernel.Cil_types.attribute ->
unitval pp_attrparam :
Format.formatter ->
Frama_c_kernel.Cil_types.attrparam ->
unitval pp_attributes :
Format.formatter ->
Frama_c_kernel.Cil_types.attributes ->
unitval pp_instr : Format.formatter -> Frama_c_kernel.Cil_types.instr -> unitval pp_label : Format.formatter -> Frama_c_kernel.Cil_types.label -> unitval pp_stmt : Format.formatter -> Frama_c_kernel.Cil_types.stmt -> unitval pp_block : Format.formatter -> Frama_c_kernel.Cil_types.block -> unitval pp_global : Format.formatter -> Frama_c_kernel.Cil_types.global -> unitval pp_file : Format.formatter -> Frama_c_kernel.Cil_types.file -> unitval pp_compinfo : Format.formatter -> Frama_c_kernel.Cil_types.compinfo -> unitval pp_logic_type_info :
Format.formatter ->
Frama_c_kernel.Cil_types.logic_type_info ->
unitval pp_logic_ctor_info :
Format.formatter ->
Frama_c_kernel.Cil_types.logic_ctor_info ->
unitval pp_initinfo : Format.formatter -> Frama_c_kernel.Cil_types.initinfo -> unitval pp_logic_info :
Format.formatter ->
Frama_c_kernel.Cil_types.logic_info ->
unitval pp_logic_constant :
Format.formatter ->
Frama_c_kernel.Cil_types.logic_constant ->
unitval pp_fundec : Format.formatter -> Frama_c_kernel.Cil_types.fundec -> unitval pp_relation : Format.formatter -> Frama_c_kernel.Cil_types.relation -> unitval pp_model_info :
Format.formatter ->
Frama_c_kernel.Cil_types.model_info ->
unitval pp_term_lval :
Format.formatter ->
Frama_c_kernel.Cil_types.term_lval ->
unitval pp_term_lhost :
Format.formatter ->
Frama_c_kernel.Cil_types.term_lhost ->
unitval pp_logic_var :
Format.formatter ->
Frama_c_kernel.Cil_types.logic_var ->
unitval pp_logic_type :
Format.formatter ->
Frama_c_kernel.Cil_types.logic_type ->
unitval pp_identified_term :
Format.formatter ->
Frama_c_kernel.Cil_types.identified_term ->
unitval pp_term : Format.formatter -> Frama_c_kernel.Cil_types.term -> unitval pp_model_field :
Format.formatter ->
Frama_c_kernel.Cil_types.model_info ->
unitval pp_term_offset :
Format.formatter ->
Frama_c_kernel.Cil_types.term_offset ->
unitval pp_logic_builtin_label :
Format.formatter ->
Frama_c_kernel.Cil_types.logic_builtin_label ->
unitval pp_logic_label :
Format.formatter ->
Frama_c_kernel.Cil_types.logic_label ->
unitval pp_builtin_logic_info :
Format.formatter ->
Frama_c_kernel.Cil_types.builtin_logic_info ->
unitval pp_extended :
Format.formatter ->
Frama_c_kernel.Cil_types.acsl_extension ->
unitval pp_short_extended :
Format.formatter ->
Frama_c_kernel.Cil_types.acsl_extension ->
unitval pp_predicate_node :
Format.formatter ->
Frama_c_kernel.Cil_types.predicate_node ->
unitval pp_predicate :
Format.formatter ->
Frama_c_kernel.Cil_types.predicate ->
unitval pp_toplevel_predicate :
Format.formatter ->
Frama_c_kernel.Cil_types.toplevel_predicate ->
unitval pp_identified_predicate :
Format.formatter ->
Frama_c_kernel.Cil_types.identified_predicate ->
unitval pp_code_annotation :
Format.formatter ->
Frama_c_kernel.Cil_types.code_annotation ->
unitval pp_funspec : Format.formatter -> Frama_c_kernel.Cil_types.funspec -> unitval pp_behavior :
Format.formatter ->
Frama_c_kernel.Cil_types.funbehavior ->
unitval pp_global_annotation :
Format.formatter ->
Frama_c_kernel.Cil_types.global_annotation ->
unitval pp_decreases : Format.formatter -> Frama_c_kernel.Cil_types.variant -> unitval pp_variant : Format.formatter -> Frama_c_kernel.Cil_types.variant -> unitval pp_from : Format.formatter -> Frama_c_kernel.Cil_types.from -> unitval pp_assigns : Format.formatter -> Frama_c_kernel.Cil_types.assigns -> unitval pp_allocation :
Format.formatter ->
Frama_c_kernel.Cil_types.allocation ->
unitval pp_loop_from : Format.formatter -> Frama_c_kernel.Cil_types.from -> unitval pp_loop_assigns :
Format.formatter ->
Frama_c_kernel.Cil_types.assigns ->
unitval pp_loop_allocation :
Format.formatter ->
Frama_c_kernel.Cil_types.allocation ->
unitval pp_post_cond :
Format.formatter ->
(Frama_c_kernel.Cil_types.termination_kind
* Frama_c_kernel.Cil_types.identified_predicate) ->
unitval pp_full_assigns :
string ->
Format.formatter ->
Frama_c_kernel.Cil_types.assigns ->
unitfirst parameter is the introducing keyword (e.g. loop_assigns or assigns).
val without_annot :
(Format.formatter -> 'a -> unit) ->
Format.formatter ->
'a ->
unitwithout_annot printer fmt x pretty prints x by using printer, without pretty-printing its function contracts and code annotations.
val force_brace :
(Format.formatter -> 'a -> unit) ->
Format.formatter ->
'a ->
unitself#force_brace printer fmt x pretty prints x by using printer, but add some extra braces '{' and '}' which are hidden by default.
val with_unfold_precond :
(Frama_c_kernel.Cil_types.stmt -> bool) ->
(Format.formatter -> 'a -> unit) ->
Format.formatter ->
'a ->
unit