Module Wp.WpReport

Export Statistics.

Patterns for formatting:

Patterns in fct:

Patterns in main:

Prover strings are "wp", "ergo", "coq" , "z3" and "simplify". Format strings are "100" (percents of valid upon total, default), "total", "valid" and "failed" for respective number of verification conditions. Zero is printed as zero. Percentages are printed in decimal "dd.d".

type fcstat
val fcstat : unit -> fcstat
val export : fcstat -> Frama_c_kernel.Filepath.t -> unit
val export_json : fcstat -> ?jinput:string -> joutput:string -> unit -> unit