]> git.ipfire.org Git - thirdparty/gcc.git/commitdiff
ada: Fix SPARK context discovery from within subunits
authorPiotr Trojanek <trojanek@adacore.com>
Wed, 28 May 2025 13:42:10 +0000 (15:42 +0200)
committerMarc Poulhiès <dkm@gcc.gnu.org>
Thu, 3 Jul 2025 08:16:19 +0000 (10:16 +0200)
When navigating the AST to find the enclosing subprogram we must traverse
from subunits to the corresponding stub.

gcc/ada/ChangeLog:

* lib-xref-spark_specific.adb
(Enclosing_Subprogram_Or_Library_Package): Traverse subunits and body
stubs.

gcc/ada/lib-xref-spark_specific.adb

index d77d6aa4dd02e44bef2e516f67a492f9683b6285..03693a96bae7b969b718180594f9c7badb48f419 100644 (file)
@@ -258,6 +258,13 @@ package body SPARK_Specific is
                Context := Defining_Entity (Context);
                exit;
 
+            when N_Subunit =>
+               Context := Corresponding_Stub (Context);
+
+            when N_Body_Stub =>
+               Context := Corresponding_Spec_Of_Stub (Context);
+               exit;
+
             when others =>
                Context := Parent (Context);
          end case;