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

Yannick Moy moy at adacore.com
Mon Nov 14 17:46:58 CET 2011


We currently prove an Ada subprogram by generating a corresponding Why
subprogram, from which all VCs related to functional properties (subprogram
contract, loop invariants, assertions) and all VCs related to runtime errors are
generated. It appears that the Why code generated for runtime-error checks is
the main cause for alt-ergo to fail proving functional VCs in a given time.

This is unfortunate, because the code for runtime-error checks is of the form:

  ___ignore(<Why code for checking absence of runtime errors in an expression>)

where ignore takes whatever and returns unit:

  function ___ignore 'a : ()

So it is completely useless to take this into account when generating a VC for
some code outside this call.

I wondered if this is a problem others face, and if there could be a way to have
a special "ignore" construct in Why, so that VCs never contain in their context
the hypotheses for such ignored blocks.

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

Best regards,

More information about the Why3-club mailing list