Skip to content

Commit

Permalink
Merge branch 'topic/gnatkp_exemptions' into 'master'
Browse files Browse the repository at this point in the history
Split GNATkp exemptions from others

Closes #336

See merge request eng/libadalang/langkit-query-language!307
  • Loading branch information
HugoGGuerrier committed Nov 8, 2024
2 parents 6ce303c + 4b78607 commit f72fba3
Show file tree
Hide file tree
Showing 7 changed files with 105 additions and 5 deletions.
20 changes: 19 additions & 1 deletion lkql_checker/doc/gnatcheck_rm/using_gnatcheck.rst
Original file line number Diff line number Diff line change
Expand Up @@ -960,9 +960,27 @@ combined with the ``--kp-version`` and possibly ``--target`` switches,
.. attention::

You must provide explicit target and runtime (either through the command-line
or with a provided project file) when running GNATKP to ensure the result
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
Expand Down
12 changes: 10 additions & 2 deletions lkql_checker/src/gnatcheck-diagnoses.adb
Original file line number Diff line number Diff line change
Expand Up @@ -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;

---------------------------
Expand Down Expand Up @@ -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
Expand Down
10 changes: 8 additions & 2 deletions lkql_checker/src/gnatcheck-diagnoses.ads
Original file line number Diff line number Diff line change
Expand Up @@ -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 --
Expand Down
3 changes: 3 additions & 0 deletions testsuite/tests/gnatcheck/exemptions/gnatkp/prj.gpr
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
project Prj is
for Source_Dirs use ("src");
end Prj;
30 changes: 30 additions & 0 deletions testsuite/tests/gnatcheck/exemptions/gnatkp/src/main.adb
Original file line number Diff line number Diff line change
@@ -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;
23 changes: 23 additions & 0 deletions testsuite/tests/gnatcheck/exemptions/gnatkp/test.out
Original file line number Diff line number Diff line change
@@ -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
12 changes: 12 additions & 0 deletions testsuite/tests/gnatcheck/exemptions/gnatkp/test.yaml
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit f72fba3

Please sign in to comment.