ada: Fix SPARK expansion of container aggregates

GNATprove supports container aggregates, except for indexed aggregates.
It needs all expressions to have suitable target types and Do_Range_Check
flags, which are added by the special expansion for GNATprove.

There is no impact on code generation.

gcc/ada/

	* exp_spark.adb (Expand_SPARK_N_Aggregate): New procedure for the
	special expansion.
	(Expand_SPARK): Call the new expansion procedure.
	* sem_util.adb (Is_Container_Aggregate): Implement missing test.

• [DBH] gcc/ada/exp_spark.adb
• [DBH] gcc/ada/sem_util.adb

ada: Fix spelling of functions with(out) "side effects"

Correct spelling does not include an hyphen. Fix comments and one
error message.

Also fix other mispellings of "side-effect" or "side effect" depending
on the case (adjective should have hyphen), and "side-effect-free" with
double hyphen as an adjective.

gcc/ada/

	* checks.adb, exp_aggr.adb, exp_ch4.ads, exp_ch5.adb,
	exp_util.adb, exp_util.ads, inline.adb, sem_ch13.adb,
	sem_ch6.adb, sem_ch8.adb, sem_prag.adb, sem_util.ads: Fix comments
	and typos.

• [DBH] gcc/ada/checks.adb
• [DBH] gcc/ada/exp_aggr.adb
• [DBH] gcc/ada/exp_ch4.ads
• [DBH] gcc/ada/exp_ch5.adb
• [DBH] gcc/ada/exp_util.adb
• [DBH] gcc/ada/exp_util.ads
• [DBH] gcc/ada/inline.adb
• [DBH] gcc/ada/sem_ch13.adb
• [DBH] gcc/ada/sem_ch6.adb
• [DBH] gcc/ada/sem_ch8.adb
• [DBH] gcc/ada/sem_prag.adb
• [DBH] gcc/ada/sem_util.ads

ada: Remove SPARK legality checks

SPARK legality checks apply only to code with SPARK_Mode On, and are
performed again in GNATprove for detecting SPARK-compatible declarations
in code with SPARK_Mode Auto. Remove this duplication, to only perform
SPARK legality checking in GNATprove. After this patch, only a few
special SPARK legality checks are performed in the frontend, which could
be moved to GNATprove later.

gcc/ada/

	* contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract):
	Remove checking on volatility. Remove handling of SPARK_Mode, not
	needed anymore.
	(Analyze_Entry_Or_Subprogram_Contract): Remove checking on
	volatility.
	(Check_Type_Or_Object_External_Properties): Same.
	(Analyze_Object_Contract): Same.
	* freeze.adb (Freeze_Record_Type): Same. Also remove checking on
	synchronized types and ghost types.
	* sem_ch12.adb (Instantiate_Object): Remove checking on
	volatility.
	(Instantiate_Type): Same.
	* sem_ch3.adb (Access_Type_Declaration): Same.
	(Derived_Type_Declaration): Remove checking related to untagged
	partial view.
	(Process_Discriminants): Remove checking on volatility.
	* sem_ch5.adb (Analyze_Loop_Parameter_Specification): Same.
	* sem_ch6.adb (Analyze_Procedure_Call): Fix use of SPARK_Mode
	where GNATprove_Mode was intended.
	* sem_disp.adb (Inherited_Subprograms): Protect against Empty
	node.
	* sem_prag.adb (Analyze_Global_In_Decl_Part): Remove checking on
	volatility.
	(Analyze_Pragma): Same.
	* sem_res.adb (Flag_Effectively_Volatile_Objects): Remove.
	(Resolve_Actuals): Remove checking on volatility.
	(Resolve_Entity_Name): Same.
	* sem_util.adb (Check_Nonvolatile_Function_Profile): Remove.
	(Check_Volatility_Compatibility): Remove.
	* sem_util.ads: Same.

• [DBH] gcc/ada/contracts.adb
• [DBH] gcc/ada/freeze.adb
• [DBH] gcc/ada/sem_ch12.adb
• [DBH] gcc/ada/sem_ch3.adb
• [DBH] gcc/ada/sem_ch5.adb
• [DBH] gcc/ada/sem_ch6.adb
• [DBH] gcc/ada/sem_disp.adb
• [DBH] gcc/ada/sem_prag.adb
• [DBH] gcc/ada/sem_res.adb
• [DBH] gcc/ada/sem_util.adb
• [DBH] gcc/ada/sem_util.ads

ada: Remove dependency on System.Val_Bool in System.Img_Bool

In order to facilitate the certification of System.Img_Bool, remove
its dependency on unit System.Val_Bool. Modify the definition of
ghost function Is_Boolean_Image_Ghost to take the expected boolean
value and move it to System.Val_Spec.

gcc/ada/

	* libgnat/s-imgboo.adb: Remove with_clause now in spec file.
	* libgnat/s-imgboo.ads: Remove dependency on System.Val_Bool.
	(Image_Boolean): Replace call to Value_Boolean by passing value V
	to updated ghost function Is_Boolean_Image_Ghost.
	* libgnat/s-valboo.ads (Is_Boolean_Image_Ghost): Move to other
	unit.
	(Value_Boolean.): Update precondition.
	* libgnat/s-valspe.ads (Is_Boolean_Image_Ghost): Move here. Add
	new parameter for expected boolean value.

• [DBH] gcc/ada/libgnat/s-imgboo.adb
• [DBH] gcc/ada/libgnat/s-imgboo.ads
• [DBH] gcc/ada/libgnat/s-valboo.ads
• [DBH] gcc/ada/libgnat/s-valspe.ads

ada: Fix type for SPARK expansion on deep delta aggregates

gcc/ada/

	* exp_spark.adb (Expand_SPARK_Delta_Or_Aggregate): Fix type.

• [DBH] gcc/ada/exp_spark.adb

ada: Rename Is_Limited_View to reflect actual query

Function Sem_Aux.Is_Limited_View returns whether the type is
"inherently limited" in a slightly different way from the "immutably
limited" definition in Ada 2012. Rename for clarity.

gcc/ada/

	* exp_aggr.adb: Apply the renaming.
	* exp_ch3.adb: Same.
	* exp_ch4.adb: Same.
	* exp_ch6.adb: Same.
	* exp_ch7.adb: Same.
	* exp_util.adb: Same.
	* freeze.adb: Same.
	* sem_aggr.adb: Same.
	* sem_attr.adb: Same.
	* sem_aux.adb: Alphabetize Is_Limited_Type. Rename.
	* sem_aux.ads: Same.
	* sem_ch3.adb: Apply the renaming.
	* sem_ch6.adb: Same.
	* sem_ch8.adb: Same.
	* sem_prag.adb: Same.
	* sem_res.adb: Same.
	* sem_util.adb: Same.

• [DBH] gcc/ada/exp_aggr.adb
• [DBH] gcc/ada/exp_ch3.adb
• [DBH] gcc/ada/exp_ch4.adb
• [DBH] gcc/ada/exp_ch6.adb
• [DBH] gcc/ada/exp_ch7.adb
• [DBH] gcc/ada/exp_util.adb
• [DBH] gcc/ada/freeze.adb
• [DBH] gcc/ada/sem_aggr.adb
• [DBH] gcc/ada/sem_attr.adb
• [DBH] gcc/ada/sem_aux.adb
• [DBH] gcc/ada/sem_aux.ads
• [DBH] gcc/ada/sem_ch3.adb
• [DBH] gcc/ada/sem_ch6.adb
• [DBH] gcc/ada/sem_ch8.adb
• [DBH] gcc/ada/sem_prag.adb
• [DBH] gcc/ada/sem_res.adb
• [DBH] gcc/ada/sem_util.adb

ada: Support new SPARK aspect Side_Effects

SPARK RM 6.1.11 introduces a new aspect Side_Effects to denote
those functions which may have output parameters, write global
variables, raise exceptions and not terminate. This adds support
for this aspect and the corresponding pragma in the frontend.

Handling of this aspect in the frontend is very similar to
the handling of aspect Extensions_Visible: both are Boolean
aspects whose expression should be static, they can be specified
on the same entities, with the same rule of inheritance from
overridden to overriding primitives for tagged types.

There is no impact on code generation.

gcc/ada/

	* aspects.ads: Add aspect Side_Effects.
	* contracts.adb (Add_Pre_Post_Condition)
	(Inherit_Subprogram_Contract): Add support for new contract.
	* contracts.ads: Update comments.
	* einfo-utils.adb (Get_Pragma): Add support.
	* einfo-utils.ads (Prag): Update comment.
	* errout.ads: Add explain codes.
	* par-prag.adb (Prag): Add support.
	* sem_ch13.adb (Analyze_Aspect_Specifications)
	(Check_Aspect_At_Freeze_Point): Add support.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper)
	(Analyze_Subprogram_Declaration): Call new analysis procedure to
	check SPARK legality rules.
	(Analyze_SPARK_Subprogram_Specification): New procedure to check
	SPARK legality rules. Use an explain code for the error.
	(Analyze_Subprogram_Specification): Move checks to new subprogram.
	This code was effectively dead, as the kind for parameters was set
	to E_Void at this point to detect early references.
	* sem_ch6.ads (Analyze_Subprogram_Specification): Add new
	procedure.
	* sem_prag.adb (Analyze_Depends_In_Decl_Part)
	(Analyze_Global_In_Decl_Part): Adapt legality check to apply only
	to functions without side-effects.
	(Analyze_If_Present): Extract functionality in new procedure
	Analyze_If_Present_Internal.
	(Analyze_If_Present_Internal): New procedure to analyze given
	pragma kind.
	(Analyze_Pragmas_If_Present): New procedure to analyze given
	pragma kind associated with a declaration.
	(Analyze_Pragma): Adapt support for Always_Terminates and
	Exceptional_Cases. Add support for Side_Effects. Make sure to call
	Analyze_If_Present to ensure pragma Side_Effects is analyzed prior
	to analyzing pragmas Global and Depends. Use explain codes for the
	errors.
	* sem_prag.ads (Analyze_Pragmas_If_Present): Add new procedure.
	* sem_util.adb (Is_Function_With_Side_Effects): New query function
	to determine if a function is a function with side-effects.
	* sem_util.ads (Is_Function_With_Side_Effects): Same.
	* snames.ads-tmpl: Declare new names for pragma and aspect.
	* doc/gnat_rm/implementation_defined_aspects.rst: Document new aspect.
	* doc/gnat_rm/implementation_defined_pragmas.rst: Document new pragma.
	* gnat_rm.texi: Regenerate.

• [DBH] gcc/ada/aspects.ads
• [DBH] gcc/ada/contracts.adb
• [DBH] gcc/ada/contracts.ads
• [DBH] gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
• [DBH] gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
• [DBH] gcc/ada/einfo-utils.adb
• [DBH] gcc/ada/einfo-utils.ads
• [DBH] gcc/ada/errout.ads
• [DBH] gcc/ada/gnat_rm.texi
• [DBH] gcc/ada/par-prag.adb
• [DBH] gcc/ada/sem_ch13.adb
• [DBH] gcc/ada/sem_ch6.adb
• [DBH] gcc/ada/sem_ch6.ads
• [DBH] gcc/ada/sem_prag.adb
• [DBH] gcc/ada/sem_prag.ads
• [DBH] gcc/ada/sem_util.adb
• [DBH] gcc/ada/sem_util.ads
• [DBH] gcc/ada/snames.ads-tmpl

ada: Clarify RM references that justify a constraint check

gcc/ada/

	* exp_ch5.adb (Expand_N_Case_Statement): Reference both sections
	of the Ada RM that deal with case statements and case expressions
	to justify the insertion of a runtime check.

• [DBH] gcc/ada/exp_ch5.adb

ada: Improve detection of deactivated code for warnings with -gnatwt

Switch -gnatwt is used in GNAT to track deleted code. It can be emitted
by GNAT on code that is intentionally deactivated for a given configuration.
The current test to suppress spurious warnings is not complex enough to
detect all such cases. Now improved, by using the same test as used in
GNATprove to suppress warnings related to a "statically disabled condition
which evaluates to a given value", as described in SPARK UG 7.3.2.

gcc/ada/

	* exp_util.adb (Is_Statically_Disabled): New function to detect a
	"statically disabled condition which evaluates to a given value",
	as described in SPARK UG 7.3.2.
	(Kill_Dead_Code): Call the new function Is_Statically_Disabled for
	conditions of if statements.
	* exp_util.ads (Is_Statically_Disabled): New function spec.

• [DBH] gcc/ada/exp_util.adb
• [DBH] gcc/ada/exp_util.ads