While doing Preanalysis (as is the case during ghost code handling),
some range and/or overflow checks can be saved (see Saved_Checks in
checks.adb) and later one omitted as they would be redundant (see
Find_Check in checks.adb). In the case of ghost code, the node being
Preanalyzed is a temporary copy that is discarded, so its corresponding
check is not expanded later. The node that gets expanded later is not
having any checks expanded as it is wrongly assumed it has already been
done before.
As is already the case in Preanalyze_And_Resolve, this change suppresses
all checks during Preanalyze except for GNATprove mode.
gcc/ada/
* sem.adb (Preanalyze): Suppress checks when not in GNATprove
mode.
* sem_res.adb (Preanalyze_And_Resolve): Add cross reference in
comment to above procedure.
* sinfo.ads: Typo fix in comment.