GitLab

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.