Skip to content

Commit

Permalink
Merge branch 'topic/fix_kp_u310_012' into 'master'
Browse files Browse the repository at this point in the history
Fix the KP-U310-012 detector

Closes #408

See merge request eng/libadalang/langkit-query-language!349
  • Loading branch information
HugoGGuerrier committed Jan 21, 2025
2 parents 9069e57 + 0b55301 commit 1b76381
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 1 deletion.
2 changes: 1 addition & 1 deletion lkql_checker/share/lkql/kp/KP-U310-012.lkql
Original file line number Diff line number Diff line change
Expand Up @@ -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"))
2 changes: 2 additions & 0 deletions testsuite/tests/checks/KP-U310-012/p.ads
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 1b76381

Please sign in to comment.