Despite recent changes to runtime checks for null array aggregates,
GNATprove still struggles with N_Raise_Constraint_Error nodes inserted
into AST by aggregate resolution. The ultimate fix is to move these
checks to expansion (which is disabled in GNATprove mode) and explicitly
emit a proof check in the GNATprove backend.

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

gcc/ada/

	* exp_aggr.adb (Check_Bounds): Move code and comment related to
	check for null array aggregate from Resolve_Null_Array_Aggregate.
	* sem_aggr.ads (Is_Null_Aggregate): Move spec from unit body.
	* sem_aggr.adb (Resolve_Null_Array_Aggregate): Move check to
	expansion.