vmordan
commented
5 years ago CV job statistics is rather different and most likely should not fully copy it from BenchExec. At the same time, some statistics can be exported. I think, the following statistics from BenchExec can be useful for CV:
- verifier tool options (they can be obtained from log but only for Unknowns), maybe even full job config;
- resource limitations;
- more resources (energy, blkio-w, etc.);
- quantile plot on the job page;
- scatter plot on the comparison page.
Statistics, which probably is not required in CV:
- score;
- hosts (this may be relevant, if hosts have different CPU);
- source files (they are partially shown for coverage and error traces);
- logs for safes/unsafes (too much space);
- giant comparison tables (there is a comparison page).
PavelAndrianov
It may be useful to have some general summary, as benchexec does. For instance, graphics may be a part of some report. So, the main task is to join all different csv output from several benchexec launches, and then generate an html statistics. One of the problem may be related with the same file names, which are launched with different configurations. An extension is a possibility to join and compare different jobs.