r273348 - in /trunk/gcc/ada: ChangeLog sem_spar...

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Wed Jul 10 09:02:36 2019
New Revision: 273348

URL: https://gcc.gnu.org/viewcvs?rev=273348&root=gcc&view=rev
Log:
[Ada] Fix possible crashes in GNATprove analysis of pointers

The new analysis of SPARK pointer rules could crash on some constructs.
Now fixed.

There is no impact on compilation.

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

gcc/ada/

	* sem_spark.adb (Check_Expression): Allow digits constraints as
	input.
	(Illegal_Global_Usage): Pass in the entity.
	(Is_Subpath_Expression): New function to allow different nodes
	as inner parts of a path expression.
	(Read_Indexes): Allow concatenation and aggregates with box
	expressions.  Allow attributes Update and Loop_Entry.
	(Check_Expression): Allow richer membership test.
	(Check_Node): Ignore bodies of generics.
	(Get_Root_Object): Allow concatenation and attributes.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/sem_spark.adb