Merge branch 'topic/209' into 'master'

Fix SPARK_Procedures_Without_Globals

Closes #209

See merge request eng/libadalang/langkit-query-language!163

lkql_checker/doc/gnatcheck_rm/predefined_rules.rst

@@ -4133,15 +4133,15 @@ This rule has the following (optional) parameter for the ``+R`` option:
 .. code-block:: ada
    :emphasize-lines: 9
 
-package Pack is
-   procedure Proc (P1 : out Integer; P2 : in out Integer);
-   type Arr is array (1 .. 10 ) of Integer;
-end Pack;
+    package Pack is
+       procedure Proc (P1 : out Integer; P2 : in out Integer);
+       type Arr is array (1 .. 10 ) of Integer;
+    end Pack;
 
-with Pack; use Pack;
-procedure Proc (X : in out Arr; I, J : Integer) is
-begin
-   Proc (X (I), X (J));   --  FLAG
+    with Pack; use Pack;
+    procedure Proc (X : in out Arr; I, J : Integer) is
+    begin
+       Proc (X (I), X (J));   --  FLAG
 
 
 .. _Profile_Discrepancies:
@@ -8044,6 +8044,37 @@ This rule has no parameters.
       raise Constraint_Error;    --  FLAG
 
 
+.. _SPARK_Procedures_Without_Globals:
+
+``SPARK_Procedures_Without_Globals``
+------------------------------------
+
+.. index:: Separates
+
+Flags SPARK procedures that don't have a global aspect.
+
+This rule has no parameters.
+
+.. rubric:: Example
+
+.. code-block:: ada
+
+   package Test is
+       procedure P with SPARK_Mode => On; -- FLAG
+
+       procedure Q is null; -- NOFLAG
+
+       function Foo return Integer  -- NOFLAG
+       is (12)
+       with SPARK_Mode => On;
+
+       V : Integer;
+
+       procedure T with Global => V;  -- NOFLAG
+
+       function Bar return Integer with SPARK_Mode => On;  -- NOFLAG
+   end Test;
+
 .. _Separates:
 
 ``Separates``

lkql_checker/share/lkql/spark_procedures_without_globals.lkql

@@ -1,8 +1,9 @@
 import stdlib
 
-@check(message="SPARK subprogram doesn't have a Global aspect",
+@check(message="SPARK procedure doesn't have a Global aspect",
        category="Style", subcategory="Programming Practice")
 fun spark_procedures_without_globals(node) =
     |" Check that every SPARK subprogram has a Global aspect
-    (node is BasicSubpDecl(p_has_spark_mode_on() is true))
+    (node is BasicSubpDecl(p_has_spark_mode_on() is true,
+                           p_subp_decl_spec() is BaseSubpSpec(p_return_type() is null)))
     and not node.p_has_aspect("Global")

testsuite/tests/checks/spark_procedures_without_globals/test.adb

@@ -8,4 +8,9 @@ package body Test with SPARK_Mode => On is
    begin
       null;
    end T;
+
+   function Bar return Integer is
+   begin
+      return 12;
+   end Bar;
 end Test;

testsuite/tests/checks/spark_procedures_without_globals/test.ads

@@ -11,4 +11,6 @@ package Test is
    V : Integer;
 
    procedure T with Global => V;  -- NOFLAG
+
+   function Bar return Integer with SPARK_Mode => On;  -- NOFLAG
 end Test;

testsuite/tests/checks/spark_procedures_without_globals/test.out

@@ -1,4 +1,4 @@
-test.ads:3:14: rule violation: SPARK subprogram doesn't have a Global aspect
+test.ads:3:14: rule violation: SPARK procedure doesn't have a Global aspect
 3 |    procedure P with SPARK_Mode => On; -- FLAG
   |              ^