Fix KP-U310-012 detector

AdaCore · Jan 21, 2025 · 0b55301 · 0b55301
1 parent 9069e57
commit 0b55301
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git 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
@@ -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