From b7e875ce96282a9c4ecc6cfd4f043c1039e5b7e3 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Tue, 21 Aug 2018 14:44:30 +0000 Subject: [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 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 --- gcc/ada/lib-xref-spark_specific.adb | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 0ce834a..00fe71a 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 -- cgit v1.1