Frama-C API - engine
method name : env -> Wp__.Lang.F.term -> string
Printer Components
Generate a name for marked term
method pp_clause : string Qed.Plib.printer
Default: "@{<wp:clause>...}"
method pp_stmt : string Qed.Plib.printer
Default: "@{<wp:stmt>...}"
method pp_comment : string Qed.Plib.printer
Default: "@{<wp:comment>(* ... *)}"
method pp_property : Frama_c_kernel.Property.t Qed.Plib.printer
Default: "@{<wp:property>(* ... *)}"
method pp_warning : Wp__.Warning.t Qed.Plib.printer
Default: "@{<wp:warning>Warning}..."
method pp_name : string Qed.Plib.printer
Default: Format.pp_print_string
method pp_core : Wp__.Lang.F.term Qed.Plib.printer
Default: plang#pp_sort
method pp_intro : clause:string -> ?dot:string -> Wp__.Lang.F.pred Qed.Plib.printer
method pp_condition : Wp__.Conditions.step Qed.Plib.printer
method pp_block : clause:string -> Wp__.Conditions.sequence Qed.Plib.printer
method pp_goal : Wp__.Lang.F.pred Qed.Plib.printer
method pp_step : Wp__.Conditions.step Qed.Plib.printer
Assumes an "<hv>" box is opened.
method pp_block : clause:string -> Wp__.Conditions.sequence Qed.Plib.printer
Assumes an "<hv>" box is opened and all variables are named.
method pp_sequence : clause:string -> Wp__.Conditions.sequence Qed.Plib.printer
Assumes an "<hv>" box is opened and all variables are declared. (recursively used)
method pp_sequent : Wp__.Conditions.sequent Qed.Plib.printer
Print the sequent in global environment.
method pp_esequent : env -> Wp__.Conditions.sequent Qed.Plib.printer
Print the sequent in the given environment. The environment is enriched with the shared terms.