Do not issue a warning about the postcondition of a function not
mentioning its result when this postcondition is statically True or
False, as this is a specification of non-termination (for value False)
or a hint to SPARK prover for not inlining an expression function (for
value True). In any case, the warning brings no value here.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* sem_util.adb (Check_Result_And_Post_State): Exempt trivial
	post.