[Ada] Refine description of SPARK with static Boolean expressions

[Ada] Refine description of SPARK with static Boolean expressions

A number of SPARK pragmas controlled by an optional Boolean expression
require those expressions to be static. This is now clarified in the
GNAT RM.

gcc/ada/

	* doc/gnat_rm/implementation_defined_pragmas.rst
	(Abstract_State, Async_Readers, Async_Writers,
	Constant_After_Elaboration, Effective_Reads, Effective_Writes,
	Extensions_Visible, Ghost, No_Caching, Volatile_Function): Only
	static Boolean expressions are allowed.
	* gnat_rm.texi: Regenerate.