module WpReport:sig..end
Patterns for formatting:
"%{cmd:arg}" or "%cmd:arg""%{cmd}" or "%cmd"fct:"%kf" or "%kf:name" the name of the function."%kf:<s>" the stats in format <s> for the function."%<p>:<s>" the stats in format <s> for prover <p>.main:<s>."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".
start chapter stats
type
val fcstat : unit -> fcstat
val export : fcstat -> string -> unitPatterns for formatting:
"%{cmd:arg}" or "%cmd:arg""%{cmd}" or "%cmd"fct:"%kf" or "%kf:name" the name of the function."%kf:<s>" the stats in format <s> for the function."%<p>:<s>" the stats in format <s> for prover <p>.main:<s>."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".