[Ada] Spurious error on pragma Unreferenced

[Pierre-Marie de Rodat]

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  <kirtc...@adacore.com>

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

gcc/testsuite/

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

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

Index: sem_prag.ads
===================================================================
--- sem_prag.ads        (revision 254563)
+++ sem_prag.ads        (working copy)
@@ -191,6 +191,8 @@
       Pragma_Remote_Types                  => False,
       Pragma_Shared_Passive                => False,
       Pragma_Task_Dispatching_Policy       => False,
+      Pragma_Unmodified                    => False,
+      Pragma_Unreferenced                  => False,
       Pragma_Warnings                      => False,
       others                               => True);
 
Index: ../testsuite/gnat.dg/unreferenced.adb
===================================================================
--- ../testsuite/gnat.dg/unreferenced.adb       (revision 0)
+++ ../testsuite/gnat.dg/unreferenced.adb       (revision 0)
@@ -0,0 +1,11 @@
+--  { dg-do compile }
+--  { dg-options "-gnatd.F" }
+
+procedure Unreferenced is
+   X : aliased Integer;
+   Y : access  Integer := X'Access;
+   Z : Integer renames Y.all;
+   pragma Unreferenced (Z);
+begin
+   null;
+end Unreferenced;