From 0b55301773f212d663fa349ea0fb970e23e20ca3 Mon Sep 17 00:00:00 2001 From: Hugo Guerrier Date: Fri, 6 Dec 2024 11:54:01 +0100 Subject: [PATCH] Fix KP-U310-012 detector --- lkql_checker/share/lkql/kp/KP-U310-012.lkql | 2 +- testsuite/tests/checks/KP-U310-012/p.ads | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/lkql_checker/share/lkql/kp/KP-U310-012.lkql b/lkql_checker/share/lkql/kp/KP-U310-012.lkql index 27261ae69..f9638f630 100644 --- a/lkql_checker/share/lkql/kp/KP-U310-012.lkql +++ b/lkql_checker/share/lkql/kp/KP-U310-012.lkql @@ -11,5 +11,5 @@ fun kp_u310_012(node) = node is SubpSpec(f_subp_kind: SubpKindFunction) when node.p_return_type() is TypeDecl(p_full_view(): ret@TypeDecl) when is_unconstrained(ret) - and (node.parent.p_has_aspect("Post") or + and (node.parent is BasicDecl(p_has_aspect("Post"): true) or ret.p_has_aspect("Type_Invariant")) diff --git a/testsuite/tests/checks/KP-U310-012/p.ads b/testsuite/tests/checks/KP-U310-012/p.ads index 4da2a9506..17f104a85 100644 --- a/testsuite/tests/checks/KP-U310-012/p.ads +++ b/testsuite/tests/checks/KP-U310-012/p.ads @@ -14,6 +14,8 @@ package P is function Create return T_Array with Post => True; -- FLAG function No_Flag return T_Array; -- NOFLAG + type F_Access is access function (B : Boolean) return String; + private type T_Array2 is array (Positive range <>) of T