diff mbox series

[Ada] Spurious error on pragma Unreferenced

Message ID 20171109115112.GA139947@adacore.com
State New
Headers show
Series [Ada] Spurious error on pragma Unreferenced | expand

Commit Message

Pierre-Marie de Rodat Nov. 9, 2017, 11:51 a.m. UTC 
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.
diff mbox series

Patch

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;