[Why3-club] [PATCH] New tool proposal: why3stats

François Bobot 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 mailing list