https://gcc.gnu.org/bugzilla/show_bug.cgi?id=127026
Andrew Teylu <andrew.teylu at vector dot com> changed:
What |Removed |Added
----------------------------------------------------------------------------
CC| |andrew.teylu at vector dot com
--- Comment #4 from Andrew Teylu <andrew.teylu at vector dot com> ---
> However, it was found while testing a verification tool I'm developing on
> real code.
>
As a note, the reduced test case is synthetic, but the construct it captures
comes from a fielded, safety-critical Ada 83 codebase. The affected routine
copies a stored record's key into a caller-supplied buffer declared out String,
i.e. an unconstrained formal, and defensively pre-clears it with a named
aggregate whose upper bound is a length read at run time from a descriptor
record. That is exactly B := (1 .. N => …) with B an unconstrained out formal
and N non-static.
Both call sites happen to pass actuals whose 'First is 1, so the misdirected
stores land where the correct ones would have; what is silently lost is the RM
5.2(11) length check. That matters: one caller's buffer length comes from a
received inter-processor message while the aggregate's bound comes from local
configuration, so the two can disagree, and the enclosing procedure has a
Constraint_Error handler that releases its locks and logs an unrecoverable
error.
On GCC 14, a mismatch reached that handler; from 15.1 it does not, and the
procedure instead returns a partially initialised buffer or writes past the end
of the actual.
