Apr 13th, 2017
Protect against unsound function contracts
When a function has an inconsistent contract (a contract which cannot hold for some inputs), GNATprove used to generate an unsound axiom which may then allow to prove anything in a caller of such a function, and so, even if the function is always called on 'valid' inputs, that is, inputs on which the contract holds. Though this behavior is expected with a proof technology such as SPARK, it used to come as a surprise to some users. We now avoid generating unsound axioms as much as possible by introducing guards for function axioms which are only assumed to hold on actually used values. Note that there are still cases where an unsound axiom will be generated (functions called in type invariants / type predicates, in primitive equalities of record types, or sometimes in user written quantified expressions). As a consequence, having inconsistent contracts on functions is still a bad usage of SPARK, and users should avoid it as much as possible. Also, this new 'safer' translation can sometimes impact proof capabilities. Thus, we provide an advanced switch --no-axiom-guard to disable it.