Skip to content

Commit b3edf1f

Browse files
raph-amiardthvnx
authored andcommitted
Fix membership_for_validity
Match `'Range` as an equivalent to `'First`/`'Last`.
1 parent bcda83a commit b3edf1f

File tree

3 files changed

+38
-14
lines changed

3 files changed

+38
-14
lines changed

lkql_checker/share/lkql/membership_for_validity.lkql

Lines changed: 30 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
# Flag each occurrence of a membership test of the form:
22
# X in Subtype_Of_X
3+
# X in Subtype_Of_X'Range
34
# X in Subtype_Of_X'First .. Subtype_Of_X'Last
45

56
fun valid_attr(node) =
@@ -22,6 +23,7 @@ fun membership_for_validity(node) =
2223
|" Two forms of membership tests are flagged:
2324
|"
2425
|" * X in Subtype_Of_X
26+
|" * X in Subtype_Of_Y'Range
2527
|" * X in Subtype_Of_X'First .. Subtype_Of_X'Last
2628
|"
2729
|" where X is a data object except for a loop parameter, and ``Subtype_Of_X``
@@ -38,17 +40,31 @@ fun membership_for_validity(node) =
3840
|" begin
3941
|" if X in My_Int then -- FLAG
4042
node is MembershipExpr(f_expr: var@Name)
41-
when not node.f_membership_exprs[2]
42-
and match node.f_membership_exprs[1]
43-
| n@Name => type_of(var) == n.p_referenced_decl()
44-
| b@BinOp(f_op: OpDoubleDot,
45-
f_left: at1@AttributeRef(f_prefix: typ1@Name)
46-
when at1.f_attribute.p_name_is("First"),
47-
f_right: at2@AttributeRef(f_prefix: typ2@Name)
48-
when at2.f_attribute.p_name_is("Last")) =>
49-
{
50-
val var_type = type_of(var);
51-
var_type == typ1.p_referenced_decl() and
52-
var_type == typ2.p_referenced_decl()
53-
}
54-
| * => false
43+
when {
44+
val type = type_of(var);
45+
46+
fun is_of_type(ref) =
47+
# Return whether ref is of the type of this MembershipExpr's expr type
48+
ref is Name(p_referenced_decl(): typ@BaseTypeDecl when typ == type);
49+
50+
type != null
51+
and not node.f_membership_exprs[2]
52+
and node.f_membership_exprs[1] is (
53+
n@Name when is_of_type(n)
54+
55+
| bin_op@BinOp(f_op: OpDoubleDot,
56+
f_left: at1@AttributeRef(f_prefix: typ1)
57+
when at1.f_attribute.p_name_is("First")
58+
and at1.f_prefix is Name,
59+
f_right: at2@AttributeRef(f_prefix: typ2)
60+
when at2.f_attribute.p_name_is("Last")
61+
and at2.f_prefix is Name)
62+
when (
63+
typ1.p_referenced_decl() == typ2.p_referenced_decl()
64+
and type == typ1.p_referenced_decl()
65+
)
66+
67+
| attr_ref@AttributeRef(f_prefix: pfx when is_of_type(pfx),
68+
f_attribute: "Range")
69+
)
70+
}

testsuite/tests/checks/membership_for_validity/test.out

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,10 @@ valid.adb:14:10: rule violation: membership test instead of 'Valid
1010
14 | elsif Y in Integer then -- FLAG
1111
| ^^^^^^^^^^^^
1212

13+
valid.adb:18:10: rule violation: membership test instead of 'Valid
14+
18 | elsif Y in Integer'Range then -- FLAG
15+
| ^^^^^^^^^^^^^^^^^^
16+
1317
Patched "valid.adb":
1418
====================
1519

@@ -30,6 +34,8 @@ begin
3034
null;
3135
elsif X in Integer then -- NOFLAG
3236
null;
37+
elsif Y 'Valid then -- FLAG
38+
null;
3339
end if;
3440
end Valid;
3541

testsuite/tests/checks/membership_for_validity/valid.adb

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,5 +15,7 @@ begin
1515
null;
1616
elsif X in Integer then -- NOFLAG
1717
null;
18+
elsif Y in Integer'Range then -- FLAG
19+
null;
1820
end if;
1921
end Valid;

0 commit comments

Comments
 (0)