From eefea4b412fc12ce176f9ff9abb09e2856dde706 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20AMIARD?= <amiard@adacore.com>
Date: Mon, 15 Jan 2024 12:04:44 +0100
Subject: [PATCH 1/2] minor doc fix

---
 .../doc/gnatcheck_rm/predefined_rules.rst      | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst b/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst
index de845254f..4a4a60c03 100644
--- a/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst
+++ b/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;
-
-with Pack; use Pack;
-procedure Proc (X : in out Arr; I, J : Integer) is
-begin
-   Proc (X (I), X (J));   --  FLAG
+    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
 
 
 .. _Profile_Discrepancies:

From 8c9489262a0fec265c3867a60e3b11334f95a297 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20AMIARD?= <amiard@adacore.com>
Date: Mon, 15 Jan 2024 11:54:49 +0100
Subject: [PATCH 2/2] Fix SPARK_Procedures_Without_Globals

Only flag procedures

Also add some documentation

Closes #209
---
 .../doc/gnatcheck_rm/predefined_rules.rst     | 31 +++++++++++++++++++
 .../spark_procedures_without_globals.lkql     |  5 +--
 .../spark_procedures_without_globals/test.adb |  5 +++
 .../spark_procedures_without_globals/test.ads |  2 ++
 .../spark_procedures_without_globals/test.out |  2 +-
 5 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst b/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst
index 4a4a60c03..8ad24f68a 100644
--- a/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst
+++ b/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst
@@ -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``
diff --git a/lkql_checker/share/lkql/spark_procedures_without_globals.lkql b/lkql_checker/share/lkql/spark_procedures_without_globals.lkql
index 30112b8dd..ab5135114 100644
--- a/lkql_checker/share/lkql/spark_procedures_without_globals.lkql
+++ b/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")
diff --git a/testsuite/tests/checks/spark_procedures_without_globals/test.adb b/testsuite/tests/checks/spark_procedures_without_globals/test.adb
index 582ac7bcf..4477d9841 100644
--- a/testsuite/tests/checks/spark_procedures_without_globals/test.adb
+++ b/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;
diff --git a/testsuite/tests/checks/spark_procedures_without_globals/test.ads b/testsuite/tests/checks/spark_procedures_without_globals/test.ads
index 58fffea51..cc3f365aa 100644
--- a/testsuite/tests/checks/spark_procedures_without_globals/test.ads
+++ b/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;
diff --git a/testsuite/tests/checks/spark_procedures_without_globals/test.out b/testsuite/tests/checks/spark_procedures_without_globals/test.out
index d12ae52f3..e2a5f7aa3 100644
--- a/testsuite/tests/checks/spark_procedures_without_globals/test.out
+++ b/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
   |              ^