From: Piotr Trojanek <trojanek@adacore.com>
Date: Tue, 21 Aug 2018 14:44:30 +0000 (+0000)
Subject: [Ada] Handle pragmas that come from aspects for GNATprove
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b7e875ce96282a9c4ecc6cfd4f043c1039e5b7e3;p=gcc.git

[Ada] Handle pragmas that come from aspects for GNATprove

In GNATprove we appear to abuse a routine related to cross-references and
expect it to deliver exact results, which is not what it was designed for.

This patch is a temporary solution to avoid crashes in GNATprove; it doesn't
affect the frontend or other backends, because this code is used exclusively
by GNATprove (it is located in the frontend for technical reasons). No tests
provided.

2018-08-21  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* lib-xref.ads, lib-xref-spark_specific.adb
	(Enclosing_Subprogram_Or_Library_Package): Now roughtly works
	for pragmas that come from aspect specifications.

From-SVN: r263707
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9bbcc9d8f96..dcbec9b9320 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2018-08-21  Piotr Trojanek  <trojanek@adacore.com>
+
+	* lib-xref.ads, lib-xref-spark_specific.adb
+	(Enclosing_Subprogram_Or_Library_Package): Now roughtly works
+	for pragmas that come from aspect specifications.
+
 2018-08-21  Pierre-Marie de Rodat  <derodat@adacore.com>
 
 	* sa_messages.ads, sa_messages.adb: New source files.
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index 0ce834a616b..00fe71aecf0 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -228,7 +228,17 @@ package body SPARK_Specific is
                end loop;
 
                if Nkind (Context) = N_Pragma then
-                  Context := Parent (Context);
+                  --  When used for cross-references then aspects might not be
+                  --  yet linked to pragmas; when used for AST navigation in
+                  --  GNATprove this routine is expected to follow those links.
+
+                  if From_Aspect_Specification (Context) then
+                     Context := Corresponding_Aspect (Context);
+                     pragma Assert (Nkind (Context) = N_Aspect_Specification);
+                     Context := Entity (Context);
+                  else
+                     Context := Parent (Context);
+                  end if;
                end if;
 
             when N_Entry_Body
diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads
index 5c7a08696d6..903e64e45ec 100644
--- a/gcc/ada/lib-xref.ads
+++ b/gcc/ada/lib-xref.ads
@@ -632,6 +632,11 @@ package Lib.Xref is
       --  Return the closest enclosing subprogram or library-level package.
       --  This ensures that GNATprove can distinguish local variables from
       --  global variables.
+      --
+      --  ??? This routine should only be used for processing related to
+      --  cross-references, where it might return wrong result but must avoid
+      --  crashes on ill-formed source code. It is wrong to use it where exact
+      --  result is needed.
 
       procedure Generate_Dereference
         (N   : Node_Id;