**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.