[Why3-club] special "ignoring" construct for VC creation
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