Frama-C API - Pcond
All-in-one printers
val pretty : Conditions.sequent Qed.Plib.printer
val dump : Conditions.bundle Qed.Plib.printer
val dump_bundle : ?clause:string -> ?goal:Lang.F.pred -> Conditions.bundle Qed.Plib.printer
val dump_sequence : ?clause:string -> ?goal:Lang.F.pred -> Conditions.sequence Qed.Plib.printer
Low-level API
type env = Plang.Env.t
val alloc_hyp : Plang.pool -> (Lang.F.var -> unit) -> Conditions.sequence -> unit
val alloc_seq : Plang.pool -> (Lang.F.var -> unit) -> Conditions.sequent -> unit
Sequent Printer Engine. Uses the following CSS
:
"wp:clause"
for all clause keywords"wp:comment"
for descriptions"wp:warning"
for warnings"wp:property"
for properties
class engine : Plang.engine -> object ... end
class state : object ... end