Fix is_spark property configuration pragma handling

This change fixes a bug in the `is_spark` property where configuration
pragmas were not handled correctly: a `SPARK_Mode` configuration
pragma in a package specification only applies to the package
specification and does not affect the body (and vice-versa).

ada/ast.py

@@ -20347,7 +20347,7 @@ def local_config_pragmas():
         )
 
     @langkit_property(return_type=T.Pragma.array)
-    def sources_config_pragmas():
+    def sources_config_pragmas(include_other_part=(Bool, True)):
         """
         Return the list of configuration pragmas defined in Ada sources and
         which apply to the current unit.
@@ -20360,13 +20360,14 @@ def sources_config_pragmas():
             Cond(
                 # If Self is a spec, we need to look at its body, and
                 # conversely.
-                Self.body.is_a(T.LibraryItem),
+                include_other_part & Self.body.is_a(T.LibraryItem),
                 Self.other_part._.local_config_pragmas,
 
                 # If Self is a sub-unit, we need to look at all subunits up in
                 # the chain, the root body, and the corresponding spec.
                 Self.body.is_a(T.Subunit),
-                Self.body.cast(Subunit).root_unit._.sources_config_pragmas,
+                Self.body.cast(Subunit).root_unit
+                ._.sources_config_pragmas(include_other_part),
 
                 No(T.Pragma.array),
             )
@@ -20385,6 +20386,21 @@ def all_config_pragmas():
             .map(lambda n: n.as_bare_entity)
         )
 
+    @langkit_property(return_type=T.Pragma.entity)
+    def spark_config_pragma():
+        """
+        Return the ``SPARK_Mode`` configuration pragma that applies to the
+        current unit.
+        """
+        return (
+            Self.external_config_pragmas.concat(
+                Self.sources_config_pragmas(include_other_part=False)
+            ).filtermap(
+                lambda n: n.as_bare_entity,
+                lambda n: n.id.name_is("SPARK_Mode")
+            ).at(-1)
+        )
+
     @langkit_property(return_type=T.Pragma.entity.array, public=True)
     def config_pragmas(name=T.Symbol):
         """
@@ -20735,9 +20751,7 @@ def is_spark(include_skip_proof_annotations=(T.Bool, True)):
 
             # Finally, check for configuration pragmas. This configuration
             # pragma is of the form `pragma SPARK_Mode [On|Off|Auto]`.
-            Entity.enclosing_compilation_unit.all_config_pragmas.filter(
-                lambda p: p.id.name_is("SPARK_Mode")
-            ).at(0).then(
+            Entity.enclosing_compilation_unit.spark_config_pragma.then(
                 lambda p: p.spark_mode_is_on,
                 # No configuration pragma were found
                 default_val=False

testsuite/tests/properties/is_spark/configuration_pragma_5/test.adb

@@ -0,0 +1,3 @@
+package body Test is
+   procedure P is null; -- Off
+end Test;

testsuite/tests/properties/is_spark/configuration_pragma_5/test.ads

@@ -0,0 +1,5 @@
+pragma SPARK_Mode (On);
+
+package Test is
+   procedure P;
+end Test;

testsuite/tests/properties/is_spark/configuration_pragma_5/test.out

@@ -0,0 +1,6 @@
+=== Analysing unit:  <AnalysisUnit 'test.adb'> """
+Subprogram <NullSubpDecl ["P"] test.adb:2:4-2:24> is skipped
+
+=== Analysing unit:  <AnalysisUnit 'test2-p.adb'> """
+Subprogram <SubpBody ["P"] test2-p.adb:2:1-5:7> is analyzed
+

testsuite/tests/properties/is_spark/configuration_pragma_5/test.py

@@ -0,0 +1,22 @@
+"""
+This test checks that calling get_aspect/has_aspect/get_pragma/is_spark on a
+subprogram body node works as expected.
+"""
+import glob
+import libadalang as lal
+
+
+context = lal.AnalysisContext()
+context.set_config_pragmas_mapping(None, {})
+
+for filename in sorted(glob.glob('*.ad[bs]')):
+    unit = context.get_from_file(filename)
+    subprograms = unit.root.findall(lal.BaseSubpBody)
+    if subprograms:
+        print('=== Analysing unit: ', unit, '"""')
+        for subprogram in subprograms:
+            print("Subprogram {} is {}".format(
+                subprogram,
+                "analyzed" if subprogram.p_is_spark() else "skipped"
+            ))
+        print('')

testsuite/tests/properties/is_spark/configuration_pragma_5/test.yaml

@@ -0,0 +1 @@
+driver: python

testsuite/tests/properties/is_spark/configuration_pragma_5/test2-p.adb

@@ -0,0 +1,5 @@
+separate (Test2)
+procedure P is
+begin
+   null;
+end P;

testsuite/tests/properties/is_spark/configuration_pragma_5/test2.adb

@@ -0,0 +1,5 @@
+pragma SPARK_Mode;
+
+package body Test2 is
+   procedure P is separate;
+end Test2;

testsuite/tests/properties/is_spark/configuration_pragma_5/test2.ads

@@ -0,0 +1,5 @@
+pragma SPARK_Mode;
+
+package Test2 is
+   procedure P;
+end Test2;

user_manual/changes/libadalang/1073.yaml

@@ -0,0 +1,8 @@
+type: bugfix
+title: Fix `p_is_spark` configuration pragma handling
+description: |
+  This change fixes a bug in the `is_spark` property where configuration
+  pragmas were not handled correctly: a `SPARK_Mode` configuration pragma in a
+  package specification only applies to the package specification and does not
+  affect the body (and vice-versa).
+date: 2023-09-12