Frama-C:
Plug-ins:
Libraries:

Frama-C API - Pcond

All-in-one printers

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
class seqengine : state -> object ... end