Split GNATkp exemptions from others

From now, GNATkp exemptions will have a separate syntax.

Author: HugoGGuerrier

lkql_checker/doc/gnatcheck_rm/using_gnatcheck.rst

@@ -963,6 +963,24 @@ combined with the ``--kp-version`` and possibly ``--target`` switches,
   or with a provided project file) when running GNATkp to ensure the result
   soundness.
 
+.. note::
+
+  The exemption mechanism is available for GNATkp as well but you have to
+  change pragmas and comments a bit to avoid conflict with GNATcheck
+  exemptions. Thus, pragmas annotations' first argument must be ``gnatkp``
+  instead of ``gnatcheck``:
+
+  .. code-block:: ada
+
+    pragma Annotate (gnatkp, Exempt_On, "kp_19198", "Justification");
+
+  And exemption comments' first word must be ``kp`` instead of ``rule``,
+  example:
+
+  .. code-block:: ada
+
+    --## kp off kp_19198 ## Justification
+
 You can check via the GNAT Tracker interface which known problems are
 relevant to your version of GNAT and your target before deciding which
 known problems may impact you: most known problems are only relevant to a

lkql_checker/src/gnatcheck-diagnoses.adb

@@ -1913,11 +1913,15 @@ package body Gnatcheck.Diagnoses is
    is
       Pragma_Name : constant Text_Type := To_Lower (El.F_Id.Text);
       Pragma_Args : constant LAL.Analysis.Base_Assoc_List := El.F_Args;
+      Tool_Name   : constant Text_Type :=
+        (if Gnatkp_Mode
+         then "gnatkp"
+         else "gnatcheck");
    begin
       return Pragma_Name in "annotate" | "gnat_annotate"
          and then not Pragma_Args.Is_Null
          and then To_Lower
-           (Pragma_Args.List_Child (1).P_Assoc_Expr.Text) = "gnatcheck";
+           (Pragma_Args.List_Child (1).P_Assoc_Expr.Text) = Tool_Name;
    end Is_Exemption_Pragma;
 
    ---------------------------
@@ -2236,7 +2240,11 @@ package body Gnatcheck.Diagnoses is
          return;
       end if;
 
-      Match (Match_Exempt_Comment, Text, Matches);
+      if Gnatkp_Mode then
+         Match (Match_Kp_Exempt_Comment, Text, Matches);
+      else
+         Match (Match_Rule_Exempt_Comment, Text, Matches);
+      end if;
 
       if Matches (0) = No_Match then
          --  We don't issue a warning here, because, it's possible (however

lkql_checker/src/gnatcheck-diagnoses.ads

@@ -43,8 +43,14 @@ package Gnatcheck.Diagnoses is
    Match_Rule_Warning_Param : constant Pattern_Matcher :=
      Compile ("(\.?\w)");
 
-   Match_Exempt_Comment : constant Pattern_Matcher :=
-     Compile ("--##\s*rule\s+(line\s+)?(on|off)\s+([^\s]+)[^#]*(?:##(.*))?");
+   Common_Exempt_Comment_Match : constant String :=
+     "\s+(line\s+)?(on|off)\s+([^\s]+)[^#]*(?:##(.*))?";
+
+   Match_Rule_Exempt_Comment : constant Pattern_Matcher :=
+     Compile ("--##\s*rule" & Common_Exempt_Comment_Match);
+
+   Match_Kp_Exempt_Comment : constant Pattern_Matcher :=
+     Compile ("--##\s*kp" & Common_Exempt_Comment_Match);
 
    -----------------------
    -- Diagnoses storage --

testsuite/tests/gnatcheck/exemptions/gnatkp/prj.gpr

@@ -0,0 +1,3 @@
+project Prj is
+   for Source_Dirs use ("src");
+end Prj;

testsuite/tests/gnatcheck/exemptions/gnatkp/src/main.adb

@@ -0,0 +1,30 @@
+procedure Main is
+   type Int_Arr is array (1 .. 3) of Integer;
+
+   X : Int_Arr;
+
+   A_1 : Int_Arr := (1, 2, 3)    --  FLAG
+     with Address => X'Address;
+
+   pragma Annotate (GnatKP, Exempt_On, "kp_19198", "Because");
+   A_2 : Int_Arr := (1, 2, 3)    --  FLAG
+     with Address => X'Address;
+   pragma Annotate (GnatKP, Exempt_Off, "kp_19198");
+
+   --## kp off kp_19198 ## Because
+   A_3 : Int_Arr := (1, 2, 3)    --  FLAG
+     with Address => X'Address;
+   --## kp on kp_19198
+begin
+   goto lbl;   --  FLAG
+
+   pragma Annotate (Gnatcheck, Exempt_On, "goto_statements", "Because");
+   goto lbl;   --  FLAG
+   pragma Annotate (Gnatcheck, Exempt_Off, "goto_statements");
+
+   --## rule off goto_statements ## Because
+   goto lbl;   --  FLAG
+   --## rule on goto_statements
+
+   <<lbl>>
+end Main;

testsuite/tests/gnatcheck/exemptions/gnatkp/test.out

@@ -0,0 +1,23 @@
+GNATcheck mode
+==============
+
+main.adb:22:04: goto statement
+   (Because)
+main.adb:26:04: goto statement
+   (Because)
+main.adb:19:04: goto statement
+   no rule exemption problems detected
+   no language violations detected
+   no internal error detected
+
+GNATKP mode
+===========
+
+main.adb:10:04: possible occurrence of KP 19198
+   (Because)
+main.adb:15:04: possible occurrence of KP 19198
+   (Because)
+main.adb:6:04: possible occurrence of KP 19198
+   no rule exemption problems detected
+   no language violations detected
+   no internal error detected

testsuite/tests/gnatcheck/exemptions/gnatkp/test.yaml

@@ -0,0 +1,12 @@
+driver: gnatcheck
+project: prj.gpr
+format: short
+tests:
+  - label: GNATcheck mode
+    mode: gnatcheck
+    rules:
+      - +Rgoto_statements
+  - label: GNATKP mode
+    mode: gnatkp
+    rules:
+      - +Rkp_19198