[Why3-club] [PATCH] New tool proposal: why3stats
bobot at lri.fr
Wed Nov 2 18:12:40 CET 2011
Le 02/11/2011 15:25, David MENTRE a écrit :
> Please find attached a new patch that implements why3stats using your
> new Session_ro module.
Patch applied (I just add a .depend for stats)
> The only missing function in Session_ro is Session.Make.get_provers to
> get the detailed information on used provers.
Reading the code, it seems to me that Session.get_provers return the
list of provers on the current computer not in the session. I added the
needed machinery in session and now session_ro gives the list of provers
registered in the session. I removed the TODO in stats.
Furthermore, stats can now handle transformations and it can accept
other configuration file with -C like why3.
I'll appreciate if you can check my changes in your code.
More information about the Why3-club