ada: Do not issue warning on postcondition in some cases
commit8912b95779dd233fb3a8c8b4dda033ed7b50be31
authorYannick Moy <moy@adacore.com>
Thu, 8 Jun 2023 09:12:25 +0000 (8 09:12 +0000)
committerMarc Poulhiès <poulhies@adacore.com>
Tue, 20 Jun 2023 07:30:50 +0000 (20 09:30 +0200)
treee8636ef3eba23725e15b2a6016ebf43c1a49031c
parentf1c15fe3f054d453f94e1412ec5bcb2c1e7205e8
ada: Do not issue warning on postcondition in some cases

Warning on suspicious postcondition is not relevant if contract
Exceptional_Cases is present, or if contract Always_Terminates is
present with a non-statically True value, as in those cases the
postcondition can be used to indicate constraints on those pre-state
for which the subprogram might terminate normally.

gcc/ada/

* sem_util.adb (Check_Result_And_Post_State): Do not warn in cases
where the warning could be spurious.
gcc/ada/sem_util.adb