Why3 configuration for Frama-C
Why3 configuration
We should clarify how we should produce the Why3 configuration file in the case of Frama-C. For opam installation we have added a message at the end of the installation but it is easy to ignore (or miss) this message. Furthermore, it is not applicable for Linux distribution packages.
One possibility for us could be to generate a Why3 configuration for Frama-C, that would always be used (unless some environment variable or option is set for example).
How to get a prover?
Currently, we use:
Why3.Whyconf.parse_filter_prover
Why3.Whyconf.filter_one_prover
However we currently can call them 3 times for each prover. One of them is due to the fact that we can have a composed name like "shortname,version,other_info", but for the two others we have a first call with the received name and the second for this same name but in lower case, and both are necessary (see: #41 (comment 99186)).
This shoul be simpler on both Frama-C and Why3 sides.