ada: Do not issue warning on postcondition in some cases

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.