diff options
| author | pmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4> | 2018-08-21 14:44:30 +0000 |
|---|---|---|
| committer | pmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4> | 2018-08-21 14:44:30 +0000 |
| commit | 4fa679e5f613bb63a45da6e728d1cf2acd55af90 (patch) | |
| tree | a9dfcb7a1ec4ecb3fe41a5b2e8d84f2d56024cef | |
| parent | cccf033e435d219cd8e0d2f5157f164892a4bc4c (diff) | |
[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.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@263707 138bc75d-0d04-0410-961f-82ee72b054a4
| -rw-r--r-- | gcc/ada/ChangeLog | 6 | ||||
| -rw-r--r-- | gcc/ada/lib-xref-spark_specific.adb | 12 | ||||
| -rw-r--r-- | gcc/ada/lib-xref.ads | 5 |
3 files changed, 22 insertions, 1 deletions
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; |