Skip to content

Commit 05cd077

Browse files
HugoGGuerrierHugoGGuerrier
committed
Add detector for KP-19853
1 parent 0cbd41d commit 05cd077

File tree

7 files changed

+151
-2
lines changed

7 files changed

+151
-2
lines changed

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

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
import stdlib
2+
3+
fun is_invalid_aspect_expr(aspect_expr, assoc_subp) =
4+
|" Return whether the provided expression which is associated to an aspect
5+
|" of ``assoc_subp`` violates the rules given in the documentation of
6+
|" ``kp_19853``.
7+
{
8+
val assoc_subp_spec = assoc_subp.p_subp_spec_or_null();
9+
val subp_params = assoc_subp_spec.p_params();
10+
from aspect_expr select first call@Name(p_is_call(): true)
11+
when call.p_referenced_decl().p_subp_spec_or_null() is call_spec@BaseSubpSpec
12+
when call_spec.p_primitive_subp_tagged_type() == assoc_subp_spec.p_primitive_subp_tagged_type()
13+
and (if call.p_is_dot_call() then call is not SingleTokNode)
14+
and stdlib.all([
15+
match actual
16+
| a@AttributeRef => not a.f_attribute.p_name_is("result")
17+
| n@Name => not n.p_referenced_decl() in subp_params
18+
| * => true
19+
for actual in [stdlib.strip_conversions(p.actual) for p in call.p_call_params()]
20+
])
21+
}
22+
23+
fun is_invalid_pre_post(aspect, assoc_subp) =
24+
|" From a given aspect object that is either a ``Pre'Class`` or a
25+
|" ``Post'Class`` of ``assoc_subp``, return whether it violates the rules
26+
|" given in the documentation of ``kp_19853``.
27+
aspect.exists
28+
and match aspect.node
29+
| pn@PragmaNode => is_invalid_aspect_expr(pn, assoc_subp)
30+
| * => is_invalid_aspect_expr(aspect.value, assoc_subp)
31+
32+
@check(help="possible occurrence of KP 19853",
33+
message="possible occurrence of KP 19853")
34+
fun kp_19853(node) =
35+
|" Flag derived type declarations whose parent type has a primitive S with
36+
|" a Pre'Class or Post'Class aspects which makes calls to a primitive
37+
|" function of S's controlling type that does not reference an S formal
38+
|" parameter (or S'Result in the case of a Post'Class).
39+
node is TypeDecl(f_type_def: DerivedTypeDef)
40+
when stdlib.any([
41+
stdlib.any([
42+
is_invalid_pre_post(p.p_get_aspect("pre'class"), p)
43+
or is_invalid_pre_post(p.p_get_aspect("post'class"), p)
44+
for p in parent.p_get_primitives()
45+
])
46+
for parent in stdlib.full_parent_types(node)
47+
])

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,10 @@
2525
"kp_19747": "24.1,24.2",
2626
"kp_19749": "24.*,25.*",
2727
"kp_19753": "21.*,22.*,23.*,24.1,24.2,25.1",
28-
"kp_19824": "25.*",
29-
"kp_19915": "25.1",
28+
"kp_19824": "22.*,23.*,24.*,25.1",
29+
"kp_19853": "25.*",
3030
"kp_19901": "24.1,24.2,25.1",
31+
"kp_19915": "25.1",
3132
"kp_ob03_009": "19.*",
3233
"kp_p226_024": "7.1.*,7.2.*,7.3.*,7.4.1,7.4.2,7.4.3",
3334
"kp_q309_014": "7.1.*,7.2.*,7.3.*,7.4.*,17.*",

‎testsuite/tests/checks/KP-19853/main.ads

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
package Main is
2+
function Process_Int (I : Integer) return Boolean is (I = 0);
3+
4+
-- Test with tagged types
5+
6+
type T_Pre is tagged null record;
7+
function F (V : T_Pre) return Integer is (0)
8+
with Pre'Class => Predicate (T_Pre'(Make));
9+
function Predicate (V : T_Pre) return Boolean is (False);
10+
function Make return T_Pre is (null record);
11+
12+
type T_Pre_Pragma is tagged null record;
13+
function F (V : T_Pre_Pragma) return Integer is (0);
14+
pragma Pre_Class (Predicate (T_Pre_Pragma'(Make)));
15+
function Predicate (V : T_Pre_Pragma) return Boolean is (False);
16+
function Make return T_Pre_Pragma is (null record);
17+
18+
type T_Post is tagged null record;
19+
function F (V : T_Post) return Integer is (0)
20+
with Post'Class => T_Post'(Make).Predicate;
21+
function Predicate (V : T_Post) return Boolean is (False);
22+
function Make return T_Post is (null record);
23+
24+
type T_Post_Pragma is tagged null record;
25+
function F (V : T_Post_Pragma) return Integer is (0);
26+
pragma Post_Class (Predicate (T_Post_Pragma'(Make)));
27+
function Predicate (V : T_Post_Pragma) return Boolean is (False);
28+
function Make return T_Post_Pragma is (null record);
29+
30+
type T_Post_Result is tagged record
31+
I : Integer;
32+
end record;
33+
function F (V : T_Post_Result) return Integer is (0)
34+
with Post'Class => T_Post_Result'(Make (F'Result)).I = 0;
35+
function Make (I : Integer) return T_Post_Result is ((I => I));
36+
37+
type T_Pre_Ref_Formal is tagged record
38+
I : Integer;
39+
end record;
40+
function F (V : T_Pre_Ref_Formal; I : Integer) return Integer is (0)
41+
with Pre'Class => T_Pre_Ref_Formal'(Make (I)).I = 0;
42+
function Make (I : Integer) return T_Pre_Ref_Formal is ((I => I));
43+
44+
type T_Pre_Ref_Prefix is tagged null record;
45+
function F (V : T_Pre_Ref_Prefix) return Integer is (0)
46+
with Pre'Class => V.Predicate;
47+
function Predicate (V : T_Pre_Ref_Prefix) return Boolean is (False);
48+
49+
type T_Pre_No_Prim_Call is tagged null record;
50+
function F (V : T_Pre_No_Prim_Call) return Integer is (0)
51+
with Pre'Class => Process_Int (0);
52+
53+
type T_Pre_No_Call is tagged null record;
54+
function F (V : T_Pre_No_Call) return Integer is (0)
55+
with Pre'Class => False;
56+
57+
type T_Pre_Not_Class is tagged null record;
58+
function F (V : T_Pre_Not_Class) return Integer is (0)
59+
with Pre => Predicate (T_Pre_Not_Class'(Make));
60+
function Predicate (V : T_Pre_Not_Class) return Boolean is (False);
61+
function Make return T_Pre_Not_Class is (null record);
62+
63+
type Child_Pre is new T_Pre with null record; -- FLAG
64+
type Child_Child_Pre is new Child_Pre with null record; -- FLAG
65+
type Child_Pre_Pragma is new T_Pre_Pragma with null record; -- FLAG
66+
type Child_Post is new T_Post with null record; -- FLAG
67+
type Child_Post_Pragma is new T_Post_Pragma with null record; -- FLAG
68+
type Child_Post_Result is new T_Post_Result with null record; -- NOFLAG
69+
type Child_Pre_Ref_Formal is new T_Pre_Ref_Formal with null record; -- NOFLAG
70+
type Child_Pre_Ref_Prefix is new T_Pre_Ref_Prefix with null record; -- NOFLAG
71+
type Child_No_Prim_Call is new T_Pre_No_Prim_Call with null record; -- NOFLAG
72+
type Child_Pre_No_Call is new T_Pre_No_Call with null record; -- NOFLAG
73+
type Child_Pre_Not_Class is new T_Pre_Not_Class with null record; -- NOFLAG
74+
end Main;

‎testsuite/tests/checks/KP-19853/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-19853/test.out

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
main.ads:63:9: rule violation: possible occurrence of KP 19853
2+
63 | type Child_Pre is new T_Pre with null record; -- FLAG
3+
| ^^^^^^^^^
4+
5+
main.ads:64:9: rule violation: possible occurrence of KP 19853
6+
64 | type Child_Child_Pre is new Child_Pre with null record; -- FLAG
7+
| ^^^^^^^^^^^^^^^
8+
9+
main.ads:65:9: rule violation: possible occurrence of KP 19853
10+
65 | type Child_Pre_Pragma is new T_Pre_Pragma with null record; -- FLAG
11+
| ^^^^^^^^^^^^^^^^
12+
13+
main.ads:66:9: rule violation: possible occurrence of KP 19853
14+
66 | type Child_Post is new T_Post with null record; -- FLAG
15+
| ^^^^^^^^^^
16+
17+
main.ads:67:9: rule violation: possible occurrence of KP 19853
18+
67 | type Child_Post_Pragma is new T_Post_Pragma with null record; -- FLAG
19+
| ^^^^^^^^^^^^^^^^^
20+

‎testsuite/tests/checks/KP-19853/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_19853
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_19853" label="possible occurrence of KP 19853"/>
9596
<check switch="+Rkp_19901" label="possible occurrence of KP 19901"/>
9697
<check switch="+Rkp_19915" label="occurrence of KP 19915"/>
9798
<check switch="+Rkp_ob03_009" label="possible occurrence of KP OB03-009"/>
@@ -611,6 +612,7 @@ testsuite_driver: No output file generated by gnatcheck
611612
<check switch="+Rkp_19749" label="possible occurrence of KP 19749"/>
612613
<check switch="+Rkp_19753" label="possible occurrence of KP 19753"/>
613614
<check switch="+Rkp_19824" label="possible occurrence of KP 19824"/>
615+
<check switch="+Rkp_19853" label="possible occurrence of KP 19853"/>
614616
<check switch="+Rkp_19901" label="possible occurrence of KP 19901"/>
615617
<check switch="+Rkp_19915" label="occurrence of KP 19915"/>
616618
<check switch="+Rkp_ob03_009" label="possible occurrence of KP OB03-009"/>

0 commit comments

Comments
 (0)