[Why3-club] special "ignoring" construct for VC creation

Yannick Moy moy at adacore.com
Wed Nov 16 17:26:27 CET 2011

On 11/14/2011 05:46 PM, Yannick Moy wrote:

> Otherwise, the workaround is simply to generate two different Why programs for
> the functional properties and the runtime errors, like done in Frama-C.

Thinking more about that, this is only a half-baked solution, as we will still
get all the useless hypotheses in the context of VCs for run-time errors. So
having something at the VC creation (splitting) level would be much better.

More information about the Why3-club mailing list