Re: Hi-Lite high integrity showcase and overflow errors

[Florian Weimer <fw@deneb.enyo.de>]

* yannick moy:

> Indeed, the possible overflow in line 7 (the test in Mult) can be
> raised at run-time, hence the overflow check failure when compiling
> with -gnato.

There's recent development in this area.

In FSF GCC trunk, there is now an overflow checking mode, enabled with
-gnato3, which causes the original program to behave as expected.  In
this mode, signed integer arithmetic does not result in intermediate
overflows, and comparisons between signed integers yield the
mathemtically defined result.  In some cases, this requires arbitrary
precision arithmetic at run time, but it really helps to avoid
Constraint_Error exceptions.