Skip to content

Commit 472fa6f

Browse files
thvnxthvnx
committed
Add detector for KP-19901
1 parent dd79199 commit 472fa6f

File tree

9 files changed

+274
-0
lines changed

9 files changed

+274
-0
lines changed

‎lkql_checker/share/lkql/kp/KP-19901.lkql‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
import stdlib
2+
3+
fun defines_predicate(node) =
4+
|" If node is a BaseTypeDecl return whether the current view of node
5+
|" defines a Predicate.
6+
node is BaseTypeDecl
7+
when stdlib.any(
8+
[
9+
node.p_get_aspect_assoc(name)
10+
for name in ["Predicate", "Static_Predicate", "Dynamic_Predicate"]
11+
]
12+
) or node.p_get_pragma("Predicate")
13+
14+
fun get_predicate_aspect(node) =
15+
|" If node is a BaseTypeDecl return the associated Predicate aspect
16+
|" if one exists (whatever the aspect has been defined on node or
17+
|" any of its parents).
18+
{
19+
val predicate = node.p_get_aspect("Predicate");
20+
if predicate.exists
21+
then
22+
predicate
23+
else {
24+
val predicate = node.p_get_aspect("Static_Predicate");
25+
if predicate.exists
26+
then
27+
predicate
28+
else
29+
node.p_get_aspect("Dynamic_Predicate")
30+
}
31+
}
32+
33+
fun parent_subtype(node) =
34+
|" If node is a BaseTypeDecl return its direct parent subtype.
35+
match node
36+
| st@SubtypeDecl => st.f_subtype.f_name.p_referenced_decl()
37+
| td@BaseTypeDecl => td.p_base_type()
38+
| * => null
39+
40+
fun associated_decl(aspect) =
41+
|" Return the syntactic node that defines the aspect.
42+
match aspect.node
43+
| aa@AspectAssoc => aa.p_parent_basic_decl()
44+
| p@PragmaNode => p.p_associated_entities()[1]?.p_parent_basic_decl()
45+
| * => null
46+
47+
fun private_parent_with_predicate(node) =
48+
|" Return whether one parent subtype of node is private and defines a Predicate.
49+
match parent_subtype(node)
50+
| p@BaseTypeDecl => {
51+
val aspect = get_predicate_aspect(p);
52+
aspect.exists
53+
and stdlib.any(
54+
[p.p_is_private() for p in associated_decl(aspect)?.p_all_parts()]
55+
)
56+
or private_parent_with_predicate(associated_decl(aspect))
57+
}
58+
| null => false
59+
60+
@check(help="possible occurrence of KP 19901",
61+
message="possible occurrence of KP 19901")
62+
fun kp_19901(node) =
63+
|" Check for subtype declarations that include a predicate aspect
64+
|" specification. Check the type or subtype named in the subtype_mark of
65+
|" the subtype declaration to see whether it is already subject to a
66+
|" predicate and has a partial view (that is, has an "is private" or
67+
|" "with private" declaration).
68+
node is BaseTypeDecl
69+
when defines_predicate(node)
70+
and private_parent_with_predicate(node)

‎lkql_checker/share/lkql/kp/kp.json‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@
2727
"kp_19753": "21.*,22.*,23.*,24.1,24.2,25.1",
2828
"kp_19824": "25.*",
2929
"kp_19915": "25.1",
30+
"kp_19901": "24.1,24.2,25.1",
3031
"kp_ob03_009": "19.*",
3132
"kp_p226_024": "7.1.*,7.2.*,7.3.*,7.4.1,7.4.2,7.4.3",
3233
"kp_q309_014": "7.1.*,7.2.*,7.3.*,7.4.*,17.*",

‎testsuite/tests/checks/KP-19901/main.adb‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
procedure Main is
2+
package Test is
3+
type P0 is tagged null record; -- NOFLAG
4+
type P1 is tagged null record with Predicate => True; -- NOFLAG
5+
type P2 is tagged private; -- NOFLAG
6+
type P3 is new P0 with private with Predicate => True; -- NOFLAG
7+
type P4 is new P1 with private with Predicate => True; -- NOFLAG
8+
type P6 is tagged private; -- NOFLAG
9+
private
10+
type P2 is tagged null record with Predicate => True; -- NOFLAG
11+
type P3 is new P0 with null record; -- NOFLAG
12+
type P4 is new P1 with null record; -- NOFLAG
13+
type P5 is new P2 with null record with Predicate => True; -- FLAG
14+
type P6 is tagged null record; -- NOFLAG
15+
pragma Predicate (P6, True);
16+
end Test;
17+
18+
package body Test is
19+
end Test;
20+
21+
subtype S0 is Test.P0 with Predicate => True; -- NOFLAG
22+
subtype S1 is Test.P1 with Predicate => True; -- NOFLAG
23+
subtype S2 is Test.P2 with Predicate => True; -- FLAG
24+
subtype S3 is Test.P3 with Predicate => True; -- FLAG
25+
subtype S4 is Test.P4 with Predicate => True; -- FLAG
26+
subtype S5 is S4; -- NOFLAG
27+
subtype S6 is Test.P2; -- NOFLAG
28+
subtype S7 is S6 with Predicate => True; -- FLAG
29+
30+
type T0 is new Test.P0 with null record with Predicate => True; -- NOFLAG
31+
type T1 is new Test.P1 with null record with Predicate => True; -- NOFLAG
32+
type T2 is new Test.P2 with null record with Predicate => True; -- FLAG
33+
type T3 is new Test.P3 with null record with Predicate => True; -- FLAG
34+
type T4 is new Test.P4 with null record with Predicate => True; -- FLAG
35+
type T5 is new T4 with null record; -- NOFLAG
36+
type T6 is new Test.P2 with null record; -- NOFLAG
37+
type T7 is new T6 with null record with Predicate => True; -- FLAG
38+
39+
subtype S8 is S6; -- NOFLAG
40+
type T8 is new S8 with null record with Predicate => True; -- FLAG
41+
42+
type T9 is new Test.P6 with null record with Predicate => True; -- FLAG
43+
type T10 is new Test.P2 with null record; -- FLAG
44+
pragma Predicate (T10, True);
45+
begin
46+
null;
47+
end;

‎testsuite/tests/checks/KP-19901/main_dynamic.adb‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
procedure Main_Dynamic is
2+
package Test is
3+
type P0 is tagged null record; -- NOFLAG
4+
type P1 is tagged null record with Dynamic_Predicate => True; -- NOFLAG
5+
type P2 is tagged private; -- NOFLAG
6+
type P3 is new P0 with private with Dynamic_Predicate => True; -- NOFLAG
7+
type P4 is new P1 with private with Dynamic_Predicate => True; -- NOFLAG
8+
private
9+
type P2 is tagged null record with Dynamic_Predicate => True; -- NOFLAG
10+
type P3 is new P0 with null record; -- NOFLAG
11+
type P4 is new P1 with null record; -- NOFLAG
12+
type P5 is new P2 with null record with Dynamic_Predicate => True; -- FLAG
13+
end Test;
14+
15+
package body Test is
16+
end Test;
17+
18+
subtype S0 is Test.P0 with Dynamic_Predicate => True; -- NOFLAG
19+
subtype S1 is Test.P1 with Dynamic_Predicate => True; -- NOFLAG
20+
subtype S2 is Test.P2 with Dynamic_Predicate => True; -- FLAG
21+
subtype S3 is Test.P3 with Dynamic_Predicate => True; -- FLAG
22+
subtype S4 is Test.P4 with Dynamic_Predicate => True; -- FLAG
23+
subtype S5 is S4; -- NOFLAG
24+
subtype S6 is Test.P2; -- NOFLAG
25+
subtype S7 is S6 with Dynamic_Predicate => True; -- FLAG
26+
27+
type T0 is new Test.P0 with null record with Dynamic_Predicate => True; -- NOFLAG
28+
type T1 is new Test.P1 with null record with Dynamic_Predicate => True; -- NOFLAG
29+
type T2 is new Test.P2 with null record with Dynamic_Predicate => True; -- FLAG
30+
type T3 is new Test.P3 with null record with Dynamic_Predicate => True; -- FLAG
31+
type T4 is new Test.P4 with null record with Dynamic_Predicate => True; -- FLAG
32+
type T5 is new T4 with null record; -- NOFLAG
33+
type T6 is new Test.P2 with null record; -- NOFLAG
34+
type T7 is new T6 with null record with Dynamic_Predicate => True; -- FLAG
35+
36+
subtype S8 is S6; -- NOFLAG
37+
type T8 is new S8 with null record with Dynamic_Predicate => True; -- FLAG
38+
begin
39+
null;
40+
end;

‎testsuite/tests/checks/KP-19901/main_static.adb‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
procedure Main_Static is
2+
package Test is
3+
type P0 is new String (1 .. 1) with Static_Predicate => True; -- NOFLAG
4+
type P1 is private; -- NOFLAG
5+
private
6+
type P1 is new String (1 .. 2) with Static_Predicate => True; -- NOFLAG
7+
end Test;
8+
9+
package body Test is
10+
end Test;
11+
12+
subtype S0 is Test.P0 with Dynamic_Predicate => True; -- NOFLAG
13+
type T0 is new Test.P0 with Dynamic_Predicate => True; -- NOFLAG
14+
type T1 is new Test.P1 with Dynamic_Predicate => True; -- FLAG
15+
begin
16+
null;
17+
end;

‎testsuite/tests/checks/KP-19901/prj.gpr‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
project Prj is
2+
end Prj;

‎testsuite/tests/checks/KP-19901/test.out‎

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
main.adb:13:12: rule violation: possible occurrence of KP 19901
2+
13 | type P5 is new P2 with null record with Predicate => True; -- FLAG
3+
| ^^
4+
5+
main.adb:23:12: rule violation: possible occurrence of KP 19901
6+
23 | subtype S2 is Test.P2 with Predicate => True; -- FLAG
7+
| ^^
8+
9+
main.adb:24:12: rule violation: possible occurrence of KP 19901
10+
24 | subtype S3 is Test.P3 with Predicate => True; -- FLAG
11+
| ^^
12+
13+
main.adb:25:12: rule violation: possible occurrence of KP 19901
14+
25 | subtype S4 is Test.P4 with Predicate => True; -- FLAG
15+
| ^^
16+
17+
main.adb:28:12: rule violation: possible occurrence of KP 19901
18+
28 | subtype S7 is S6 with Predicate => True; -- FLAG
19+
| ^^
20+
21+
main.adb:32:9: rule violation: possible occurrence of KP 19901
22+
32 | type T2 is new Test.P2 with null record with Predicate => True; -- FLAG
23+
| ^^
24+
25+
main.adb:33:9: rule violation: possible occurrence of KP 19901
26+
33 | type T3 is new Test.P3 with null record with Predicate => True; -- FLAG
27+
| ^^
28+
29+
main.adb:34:9: rule violation: possible occurrence of KP 19901
30+
34 | type T4 is new Test.P4 with null record with Predicate => True; -- FLAG
31+
| ^^
32+
33+
main.adb:37:9: rule violation: possible occurrence of KP 19901
34+
37 | type T7 is new T6 with null record with Predicate => True; -- FLAG
35+
| ^^
36+
37+
main.adb:40:9: rule violation: possible occurrence of KP 19901
38+
40 | type T8 is new S8 with null record with Predicate => True; -- FLAG
39+
| ^^
40+
41+
main.adb:42:9: rule violation: possible occurrence of KP 19901
42+
42 | type T9 is new Test.P6 with null record with Predicate => True; -- FLAG
43+
| ^^
44+
45+
main.adb:43:9: rule violation: possible occurrence of KP 19901
46+
43 | type T10 is new Test.P2 with null record; -- FLAG
47+
| ^^^
48+
49+
main_dynamic.adb:12:12: rule violation: possible occurrence of KP 19901
50+
12 | type P5 is new P2 with null record with Dynamic_Predicate => True; -- FLAG
51+
| ^^
52+
53+
main_dynamic.adb:20:12: rule violation: possible occurrence of KP 19901
54+
20 | subtype S2 is Test.P2 with Dynamic_Predicate => True; -- FLAG
55+
| ^^
56+
57+
main_dynamic.adb:21:12: rule violation: possible occurrence of KP 19901
58+
21 | subtype S3 is Test.P3 with Dynamic_Predicate => True; -- FLAG
59+
| ^^
60+
61+
main_dynamic.adb:22:12: rule violation: possible occurrence of KP 19901
62+
22 | subtype S4 is Test.P4 with Dynamic_Predicate => True; -- FLAG
63+
| ^^
64+
65+
main_dynamic.adb:25:12: rule violation: possible occurrence of KP 19901
66+
25 | subtype S7 is S6 with Dynamic_Predicate => True; -- FLAG
67+
| ^^
68+
69+
main_dynamic.adb:29:9: rule violation: possible occurrence of KP 19901
70+
29 | type T2 is new Test.P2 with null record with Dynamic_Predicate => True; -- FLAG
71+
| ^^
72+
73+
main_dynamic.adb:30:9: rule violation: possible occurrence of KP 19901
74+
30 | type T3 is new Test.P3 with null record with Dynamic_Predicate => True; -- FLAG
75+
| ^^
76+
77+
main_dynamic.adb:31:9: rule violation: possible occurrence of KP 19901
78+
31 | type T4 is new Test.P4 with null record with Dynamic_Predicate => True; -- FLAG
79+
| ^^
80+
81+
main_dynamic.adb:34:9: rule violation: possible occurrence of KP 19901
82+
34 | type T7 is new T6 with null record with Dynamic_Predicate => True; -- FLAG
83+
| ^^
84+
85+
main_dynamic.adb:37:9: rule violation: possible occurrence of KP 19901
86+
37 | type T8 is new S8 with null record with Dynamic_Predicate => True; -- FLAG
87+
| ^^
88+
89+
main_static.adb:14:9: rule violation: possible occurrence of KP 19901
90+
14 | type T1 is new Test.P1 with Dynamic_Predicate => True; -- FLAG
91+
| ^^
92+

‎testsuite/tests/checks/KP-19901/test.yaml‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
driver: checker
2+
rule_name: kp_19901
3+
project: prj.gpr

‎testsuite/tests/gnatcheck/xml_help/test.out‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,7 @@ testsuite_driver: No output file generated by gnatcheck
9292
<check switch="+Rkp_19749" label="possible occurrence of KP 19749"/>
9393
<check switch="+Rkp_19753" label="possible occurrence of KP 19753"/>
9494
<check switch="+Rkp_19824" label="possible occurrence of KP 19824"/>
95+
<check switch="+Rkp_19901" label="possible occurrence of KP 19901"/>
9596
<check switch="+Rkp_19915" label="occurrence of KP 19915"/>
9697
<check switch="+Rkp_ob03_009" label="possible occurrence of KP OB03-009"/>
9798
<check switch="+Rkp_p226_024" label="possible occurrence of KP P226-024 - global analysis required"/>
@@ -610,6 +611,7 @@ testsuite_driver: No output file generated by gnatcheck
610611
<check switch="+Rkp_19749" label="possible occurrence of KP 19749"/>
611612
<check switch="+Rkp_19753" label="possible occurrence of KP 19753"/>
612613
<check switch="+Rkp_19824" label="possible occurrence of KP 19824"/>
614+
<check switch="+Rkp_19901" label="possible occurrence of KP 19901"/>
613615
<check switch="+Rkp_19915" label="occurrence of KP 19915"/>
614616
<check switch="+Rkp_ob03_009" label="possible occurrence of KP OB03-009"/>
615617
<check switch="+Rkp_p226_024" label="possible occurrence of KP P226-024 - global analysis required"/>

0 commit comments

Comments
 (0)