[Ada] Spurious error on pragma Unreferenced

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

This patch suppresses the light expansion of references denoting renamings
that act as arguments in pragmas Unmodified and Unreferenced for GNATprove.
In general, the compiler replaces references to renamings with the renamed
name, however certain references are left as is for GNATprove. This does
not interfere with the analysis performed by the tool.

------------
-- Source --
------------

--  main.adb

procedure Main is
   X : aliased Integer;
   Y : access  Integer := X'Access;
   Z : Integer renames Y.all;
   pragma Unreferenced (Z);
begin null; end Main;

-----------------
-- Compilation --
-----------------

$ gcc -c -gnatd.F main.adb

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

gcc/ada/

2017-11-09  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.ads: Add pragmas Unmodified and Unreferenced to table
	Pragma_Significant_In_SPARK.

gcc/testsuite/

2017-11-09  Hristian Kirtchev  <kirtchev@adacore.com>

	* gnat.dg/unreferenced.adb: New testcase.

Attachment: difs
Description: Text document