[Ada] Refactor ownership pointer checking in SPARK as a generic

[Pierre-Marie de Rodat <derodat at adacore dot com>]

Ownership checking as done in SPARK should be applied only to SPARK
code, which requires GNATprove knowledge of the SPARK_Mode boundary.
Transform the checking unit into a generic to allow passing in the
knowledge from GNATprove to that unit in GNAT sources.

Keeping the code in GNAT sources makes it possible in the future to
adapt it further (or simply instantiate it differently) to be used on
Ada code, independently of GNATprove.

There is no impact on compilation.

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

2019-07-11  Claire Dross  <dross@adacore.com>

gcc/ada/

	* gnat1drv.adb: SPARK checking rules for pointer aliasing are
	moved to GNATprove backend.
	* sem_spark.ads, sem_spark.adb (Sem_SPARK): Is now a generic
	unit. Takes as parameters:
	 - Retysp which is used to query the most underlying type
	   visible in SPARK. We do not introduce aliasing checks for
	   types which are not visibly deep.
	 - Component_Is_Visible_In_SPARK is used to avoid doing pointer
	   aliasing checks on components which are not visible in SPARK.
	 - Emit_Messages returns True in the second phase of SPARK
	   analysis. Error messages for failed aliasing checks are only
	   output in this case.
	Additionally, errors on constructs not supported in SPARK are
	removed as duplicates of marking errors. Components are stored
	in the permission map using their original component to avoid
	inconsistencies between components of different views of the
	same type.
	(Check_Expression): Handle delta constraints.
	(Is_Deep): Exported so that we can check for SPARK restrictions
	on deep types inside SPARK semantic checkings.
	(Is_Traversal_Function): Exported so that we can check for SPARK
	restrictions on traversal functions inside SPARK semantic
	checkings.
	(Check_Call_Statement, Read_Indexes): Check wether we are
	dealing with a subprogram pointer type before querying called
	entity.
	(Is_Subpath_Expression): Image attribute can appear inside a
	path.
	(Check_Loop_Statement): Correct order of statements in the loop.
	(Check_Node): Ignore raise nodes.
	(Check_Statement): Use Last_Non_Pragma to get the object
	declaration in an extended return statement.

Attachment: patch.diff.gz
Description: application/gzip