https://gcc.gnu.org/g:0fb0140c2ec957b10f550a70a616e3205927b1b5

commit r16-1925-g0fb0140c2ec957b10f550a70a616e3205927b1b5
Author: Piotr Trojanek <troja...@adacore.com>
Date:   Wed May 28 15:42:10 2025 +0200

    ada: Fix SPARK context discovery from within subunits
    
    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.

Diff:
---
 gcc/ada/lib-xref-spark_specific.adb | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/gcc/ada/lib-xref-spark_specific.adb 
b/gcc/ada/lib-xref-spark_specific.adb
index d77d6aa4dd02..03693a96bae7 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -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;

Reply via email to