From 4e7c7f30c185e5fffe7d86902bea0c1a0da86282 Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Tue, 23 May 2017 09:06:33 -0700 Subject: [PATCH] Extended transitions to universal quantified operators Reviewed By: dulmarod Differential Revision: D5094722 fbshipit-source-id: a20e96b --- infer/src/clang/cFrontend_checkers.ml | 4 +- infer/src/clang/cFrontend_errors.ml | 47 ++++++---- infer/src/clang/cTL.ml | 94 +++++++++---------- infer/src/clang/cTL.mli | 12 +-- infer/src/clang/ctl_lexer.mll | 6 +- infer/src/clang/ctl_parser.mly | 32 ++++--- .../objc/linters-for-test-only/issues.exp | 2 + .../linters-for-test-only/linters_example.al | 21 +++++ 8 files changed, 128 insertions(+), 90 deletions(-) diff --git a/infer/src/clang/cFrontend_checkers.ml b/infer/src/clang/cFrontend_checkers.ml index 3131dc45b..ace99cbe3 100644 --- a/infer/src/clang/cFrontend_checkers.ml +++ b/infer/src/clang/cFrontend_checkers.ml @@ -46,7 +46,7 @@ let tag_name_of_node an = | Ctl_parser_types.Decl decl -> Clang_ast_proj.get_decl_kind_string decl let decl_ref_or_selector_name an = - match CTL.next_state_via_transition an (Some CTL.PointerToDecl) with + match CTL.next_state_via_transition an (CTL.PointerToDecl) with | [Ctl_parser_types.Decl ObjCMethodDecl _ as decl_an] -> "The selector " ^ (Ctl_parser_types.ast_node_name decl_an) | [Ctl_parser_types.Decl _ as decl_an] -> @@ -61,7 +61,7 @@ let iphoneos_target_sdk_version _ = let available_ios_sdk an = let open Ctl_parser_types in - match CTL.next_state_via_transition an (Some CTL.PointerToDecl) with + match CTL.next_state_via_transition an (CTL.PointerToDecl) with | [Decl decl] -> (match CPredicates.get_available_attr_ios_sdk (Decl decl) with | Some version -> version diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index 37d678cd9..b3ed5f039 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -166,23 +166,36 @@ let rec apply_substitution f sub = match f with | True | False -> f - | Atomic (name, ps) -> Atomic (name, sub_list_param ps) - | Not f1 -> Not (apply_substitution f1 sub) - | And (f1, f2) -> And (apply_substitution f1 sub, apply_substitution f2 sub) - | Or (f1, f2) -> Or (apply_substitution f1 sub, apply_substitution f2 sub) - | Implies (f1, f2) -> Implies (apply_substitution f1 sub, apply_substitution f2 sub) + | Atomic (name, ps) -> + Atomic (name, sub_list_param ps) + | Not f1 -> + Not (apply_substitution f1 sub) + | And (f1, f2) -> + And (apply_substitution f1 sub, apply_substitution f2 sub) + | Or (f1, f2) -> + Or (apply_substitution f1 sub, apply_substitution f2 sub) + | Implies (f1, f2) -> + Implies (apply_substitution f1 sub, apply_substitution f2 sub) | InNode (node_type_list, f1) -> InNode (sub_list_param node_type_list, apply_substitution f1 sub) - | AU (f1, f2) -> AU (apply_substitution f1 sub, apply_substitution f2 sub) + | AU (trans, f1, f2) -> + AU (trans, apply_substitution f1 sub, apply_substitution f2 sub) | EU (trans, f1, f2) -> EU (trans, apply_substitution f1 sub, apply_substitution f2 sub) - | EF (trans, f1) -> EF (trans, apply_substitution f1 sub) - | AF f1 -> AF (apply_substitution f1 sub) - | AG f1 -> AG (apply_substitution f1 sub) - | EX (trans, f1) -> EX (trans, apply_substitution f1 sub) - | AX f1 -> AX (apply_substitution f1 sub) - | EH (cl, f1) -> EH (sub_list_param cl, apply_substitution f1 sub) - | EG (trans, f1) -> EG (trans, apply_substitution f1 sub) + | EF (trans, f1) -> + EF (trans, apply_substitution f1 sub) + | AF (trans, f1) -> + AF (trans, apply_substitution f1 sub) + | AG (trans, f1) -> + AG (trans, apply_substitution f1 sub) + | EX (trans, f1) -> + EX (trans, apply_substitution f1 sub) + | AX (trans, f1) -> + AX (trans, apply_substitution f1 sub) + | EH (cl, f1) -> + EH (sub_list_param cl, apply_substitution f1 sub) + | EG (trans, f1) -> + EG (trans, apply_substitution f1 sub) | ET (ntl, sw, f1) -> ET (sub_list_param ntl, sw, apply_substitution f1 sub) | ETX (ntl, sw, f1) -> @@ -217,13 +230,13 @@ let expand_formula phi _map _error_msg = | Or (f1, f2) -> Or (expand f1 map error_msg, expand f2 map error_msg) | Implies (f1, f2) -> Implies (expand f1 map error_msg, expand f2 map error_msg) | InNode (node_type_list, f1) -> InNode (node_type_list, expand f1 map error_msg) - | AU (f1, f2) -> AU (expand f1 map error_msg, expand f2 map error_msg) + | AU (trans, f1, f2) -> AU (trans, expand f1 map error_msg, expand f2 map error_msg) | EU (trans, f1, f2) -> EU (trans, expand f1 map error_msg, expand f2 map error_msg) | EF (trans, f1) -> EF (trans, expand f1 map error_msg) - | AF f1 -> AF (expand f1 map error_msg) - | AG f1 -> AG (expand f1 map error_msg) + | AF (trans, f1) -> AF (trans, expand f1 map error_msg) + | AG (trans, f1) -> AG (trans, expand f1 map error_msg) | EX (trans, f1) -> EX (trans, expand f1 map error_msg) - | AX f1 -> AX (expand f1 map error_msg) + | AX (trans, f1) -> AX (trans, expand f1 map error_msg) | EH (cl, f1) -> EH (cl, expand f1 map error_msg) | EG (trans, f1) -> EG (trans, expand f1 map error_msg) | ET (tl, sw, f1) -> ET (tl, sw, expand f1 map error_msg) diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 652436310..c0311ae87 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -37,13 +37,13 @@ type t = (* A ctl formula *) | Or of t * t | Implies of t * t | InNode of ALVar.alexp list * t - | AX of t + | AX of transitions option * t | EX of transitions option * t - | AF of t + | AF of transitions option * t | EF of transitions option * t - | AG of t + | AG of transitions option * t | EG of transitions option * t - | AU of t * t + | AU of transitions option * t * t | EU of transitions option * t * t | EH of ALVar.alexp list * t | ET of ALVar.alexp list * transitions option * t @@ -52,7 +52,9 @@ type t = (* A ctl formula *) let has_transition phi = match phi with | True | False | Atomic _ | Not _ | And (_, _) | Or (_, _) | Implies (_, _) | InNode (_, _) - | AX _ | AF _ | AG _ | AU (_, _) | EH (_, _) -> false + | EH (_, _) -> false + | AX (trans_opt, _) | AF (trans_opt, _) + | AG (trans_opt, _) | AU (trans_opt, _, _) | EX (trans_opt, _) | EF (trans_opt, _) | EG (trans_opt, _) | EU (trans_opt, _, _) | ET (_, trans_opt, _) | ETX (_, trans_opt, _) -> Option.is_some trans_opt @@ -127,13 +129,14 @@ module Debug = struct (Pp.comma_seq Format.pp_print_string) (nodes_to_string nl) pp_formula phi - | AX phi -> Format.fprintf fmt "AX(%a)" pp_formula phi + | AX (trs, phi) -> Format.fprintf fmt "AX[->%a](%a)" pp_transition trs pp_formula phi | EX (trs, phi) -> Format.fprintf fmt "EX[->%a](%a)" pp_transition trs pp_formula phi - | AF phi -> Format.fprintf fmt "AF(%a)" pp_formula phi + | AF (trs, phi) -> Format.fprintf fmt "AF[->%a](%a)" pp_transition trs pp_formula phi | EF (trs, phi) -> Format.fprintf fmt "EF[->%a](%a)" pp_transition trs pp_formula phi - | AG phi -> Format.fprintf fmt "AG(%a)" pp_formula phi + | AG (trs, phi) -> Format.fprintf fmt "AG[->%a](%a)" pp_transition trs pp_formula phi | EG (trs, phi) -> Format.fprintf fmt "EG[->%a](%a)" pp_transition trs pp_formula phi - | AU (phi1, phi2) -> Format.fprintf fmt "A[%a UNTIL %a]" pp_formula phi1 pp_formula phi2 + | AU (trs, phi1, phi2) -> Format.fprintf fmt "A[->%a][%a UNTIL %a]" + pp_transition trs pp_formula phi1 pp_formula phi2 | EU (trs, phi1, phi2) -> Format.fprintf fmt "E[->%a][%a UNTIL %a]" pp_transition trs pp_formula phi1 pp_formula phi2 | EH (arglist, phi) -> Format.fprintf fmt "EH[%a](%a)" @@ -520,23 +523,23 @@ let transition_decl_to_stmt d trs = let open Clang_ast_t in let temp_res = match trs, d with - | Some Body, ObjCMethodDecl (_, _, omdi) -> omdi.omdi_body - | Some Body, FunctionDecl (_, _, _, fdi) - | Some Body, CXXMethodDecl (_, _, _, fdi,_ ) - | Some Body, CXXConstructorDecl (_, _, _, fdi, _) - | Some Body, CXXConversionDecl (_, _, _, fdi, _) - | Some Body, CXXDestructorDecl (_, _, _, fdi, _) -> fdi.fdi_body - | Some Body, BlockDecl (_, bdi) -> bdi.bdi_body - | Some InitExpr, VarDecl (_, _ ,_, vdi) -> vdi.vdi_init_expr - | Some InitExpr, ObjCIvarDecl (_, _, _, fldi, _) - | Some InitExpr, FieldDecl (_, _, _, fldi) - | Some InitExpr, ObjCAtDefsFieldDecl (_, _, _, fldi)-> fldi.fldi_init_expr - | Some InitExpr, CXXMethodDecl _ - | Some InitExpr, CXXConstructorDecl _ - | Some InitExpr, CXXConversionDecl _ - | Some InitExpr, CXXDestructorDecl _ -> + | Body, ObjCMethodDecl (_, _, omdi) -> omdi.omdi_body + | Body, FunctionDecl (_, _, _, fdi) + | Body, CXXMethodDecl (_, _, _, fdi,_ ) + | Body, CXXConstructorDecl (_, _, _, fdi, _) + | Body, CXXConversionDecl (_, _, _, fdi, _) + | Body, CXXDestructorDecl (_, _, _, fdi, _) -> fdi.fdi_body + | Body, BlockDecl (_, bdi) -> bdi.bdi_body + | InitExpr, VarDecl (_, _ ,_, vdi) -> vdi.vdi_init_expr + | InitExpr, ObjCIvarDecl (_, _, _, fldi, _) + | InitExpr, FieldDecl (_, _, _, fldi) + | InitExpr, ObjCAtDefsFieldDecl (_, _, _, fldi)-> fldi.fldi_init_expr + | InitExpr, CXXMethodDecl _ + | InitExpr, CXXConstructorDecl _ + | InitExpr, CXXConversionDecl _ + | InitExpr, CXXDestructorDecl _ -> assert false (* to be done. Requires extending to lists *) - | Some InitExpr, EnumConstantDecl (_, _, _, ecdi) -> ecdi.ecdi_init_expr + | InitExpr, EnumConstantDecl (_, _, _, ecdi) -> ecdi.ecdi_init_expr | _, _ -> None in match temp_res with | Some st -> [Stmt st] @@ -588,16 +591,15 @@ let transition_decl_to_decl_via_parameters dec = List.map ~f:(fun d -> Decl d) omdi.omdi_parameters | _ -> [] -(* given a node an returns the node an' such that an transition to an' via label trans *) +(* given a node an returns a list of nodes an' such that an transition to an' via label trans *) let next_state_via_transition an trans = match an, trans with - | Decl d, Some Super -> transition_decl_to_decl_via_super d - | Decl d, Some Parameters -> transition_decl_to_decl_via_parameters d - | Decl d, Some InitExpr - | Decl d, Some Body -> transition_decl_to_stmt d trans - | Stmt st, Some Cond -> transition_stmt_to_stmt_via_condition st - | Stmt st, Some PointerToDecl -> - transition_stmt_to_decl_via_pointer st + | Decl d, Super -> transition_decl_to_decl_via_super d + | Decl d, Parameters -> transition_decl_to_decl_via_parameters d + | Decl d, InitExpr + | Decl d, Body -> transition_decl_to_stmt d trans + | Stmt st, Cond -> transition_stmt_to_stmt_via_condition st + | Stmt st, PointerToDecl -> transition_stmt_to_decl_via_pointer st | _, _ -> [] (* Evaluation of formulas *) @@ -661,12 +663,6 @@ and eval_EF phi an lcxt trans = eval_formula phi an lcxt || List.exists ~f:(fun an' -> eval_EF phi an' lcxt trans) (get_successor_nodes an) -(* Evaluate phi on node an' such that an -l-> an'. False if an' does not exists *) -and evaluate_on_transition phi an lcxt l = - let succs = next_state_via_transition an l in - List.exists ~f:(fun an' -> eval_formula phi an' lcxt) succs - - (* an, lcxt |= EX phi <=> exists an' in Successors(st): an', lcxt |= phi That is: a (an, lcxt) satifies EX phi if and only if @@ -674,10 +670,10 @@ and evaluate_on_transition phi an lcxt l = such that (an', lcxt) satifies phi *) and eval_EX phi an lcxt trans = - match trans, an with - | Some _, _ -> evaluate_on_transition phi an lcxt trans - | None, _ -> - List.exists ~f:(fun an' -> eval_formula phi an' lcxt) (get_successor_nodes an) + let succs = match trans with + | Some l -> next_state_via_transition an l + | None -> get_successor_nodes an in + List.exists ~f:(fun an' -> eval_formula phi an' lcxt) succs (* an, lcxt |= E(phi1 U phi2) evaluated using the equivalence an, lcxt |= E(phi1 U phi2) <=> an, lcxt |= phi2 or (phi1 and EX(E(phi1 U phi2))) @@ -694,8 +690,8 @@ and eval_EU phi1 phi2 an lcxt trans = Same as EU but for the all path quantifier A *) -and eval_AU phi1 phi2 an lcxt = - let f = Or (phi2, And (phi1, AX (AU (phi1, phi2)))) in +and eval_AU phi1 phi2 an lcxt trans = + let f = Or (phi2, And (phi1, AX (trans, AU (trans, phi1, phi2)))) in eval_formula f an lcxt (* an, lcxt |= InNode[node_type_list] phi <=> @@ -764,13 +760,13 @@ and eval_formula f an lcxt = not (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt) | InNode (node_type_list, f1) -> in_node node_type_list f1 an lcxt - | AU (f1, f2) -> eval_AU f1 f2 an lcxt + | AU (trans, f1, f2) -> eval_AU f1 f2 an lcxt trans | EU (trans, f1, f2) -> eval_EU f1 f2 an lcxt trans | EF (trans, f1) -> eval_EF f1 an lcxt trans - | AF f1 -> eval_formula (AU (True, f1)) an lcxt - | AG f1 -> eval_formula (Not (EF (None, (Not f1)))) an lcxt + | AF (trans, f1) -> eval_formula (AU (trans, True, f1)) an lcxt + | AG (trans, f1) -> eval_formula (Not (EF (trans, (Not f1)))) an lcxt | EX (trans, f1) -> eval_EX f1 an lcxt trans - | AX f1 -> eval_formula (Not (EX (None, (Not f1)))) an lcxt + | AX (trans, f1) -> eval_formula (Not (EX (trans, (Not f1)))) an lcxt | EH (cl, phi) -> eval_EH cl phi an lcxt | EG (trans, f1) -> (* st |= EG f1 <=> st |= f1 /\ EX EG f1 *) eval_formula (And (f1, EX (trans, (EG (trans, f1))))) an lcxt diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 53a546230..b3dbc3ba5 100644 --- a/infer/src/clang/cTL.mli +++ b/infer/src/clang/cTL.mli @@ -38,15 +38,15 @@ type t = | Or of t * t | Implies of t * t | InNode of ALVar.alexp list * t - | AX of t (** AX phi <=> for all children of the current node phi holds *) + | AX of transitions option * t (** AX phi <=> for all children of the current node phi holds *) | EX of transitions option * t (** EX phi <=> exist a child of the current node such that phi holds *) - | AF of t (** AF phi <=> for all path from the current node there is a descendant where phi holds *) + | AF of transitions option * t (** AF phi <=> for all path from the current node there is a descendant where phi holds *) | EF of transitions option * t (** EF phi <=> there exits a a path from the current node with a descendant where phi hold *) - | AG of t (** AG phi <=> for all discendant of the current node phi hold *) + | AG of transitions option * t (** AG phi <=> for all discendant of the current node phi hold *) | EG of transitions option * t (** EG phi <=> there exists a path (of descendants) from the current node where phi hold at each node of the path *) - | AU of t * t (** AU(phi1, phi2) <=> - for all paths from the current node phi1 holds in every node until ph2 holds *) + | AU of transitions option * t * t (** AU(phi1, phi2) <=> + for all paths from the current node phi1 holds in every node until ph2 holds *) | EU of transitions option * t * t (** EU(phi1, phi2) <=> there exists a path from the current node such that phi1 holds until phi2 holds *) | EH of ALVar.alexp list * t (** EH[classes]phi <=> @@ -98,7 +98,7 @@ val eval_formula : t -> ast_node -> CLintersContext.context -> bool val save_dotty_when_in_debug_mode : SourceFile.t -> unit -val next_state_via_transition : ast_node -> transitions option -> ast_node list +val next_state_via_transition : ast_node -> transitions -> ast_node list val create_ctl_evaluation_tracker : SourceFile.t -> unit diff --git a/infer/src/clang/ctl_lexer.mll b/infer/src/clang/ctl_lexer.mll index 46f3ad9d8..ab1d7f3ef 100644 --- a/infer/src/clang/ctl_lexer.mll +++ b/infer/src/clang/ctl_lexer.mll @@ -34,11 +34,11 @@ rule token = parse | "HOLDS-UNTIL" { EU } | "HOLDS-EVERYWHERE-UNTIL" { AU } | "HOLDS-EVENTUALLY" { EF } - | "HOLDS-EVENTUALLY-EVERYWHERE" { AF } + | "HOLDS-EVERYWHERE-EVENTUALLY" { AF } | "HOLDS-NEXT" { EX } | "HOLDS-EVERYWHERE-NEXT" { AX } - | "ALWAYS-HOLDS" { EG } - | "ALSWAYS-HOLDS-EVERYWHERE" { AG } + | "HOLDS-ALWAYS" { EG } + | "HOLDS-EVERYWHERE-ALWAYS" { AG } | "HOLDS-IN-SOME-SUPERCLASS-OF" { EH } | "IN-NODE" { ET } | "IN-EXCLUSIVE-NODE" { ETX } diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index 61b9c110a..f5db1f1bd 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/infer/src/clang/ctl_parser.mly @@ -189,12 +189,12 @@ actual_params: transition_label: | identifier { match $1 with - | "Body" | "body" -> Some CTL.Body - | "InitExpr" | "initexpr" -> Some CTL.InitExpr - | "Cond" | "cond" -> Some CTL.Cond - | "Parameters" | "parameters" -> Some CTL.Parameters - | "PointerToDecl" | "pointertodecl" -> Some CTL.PointerToDecl - | _ -> None } + | "Body" | "body" -> "Body", Some CTL.Body + | "InitExpr" | "initexpr" -> "InitExpr", Some CTL.InitExpr + | "Cond" | "cond" -> "Cond", Some CTL.Cond + | "Parameters" | "parameters" -> "Parameters", Some CTL.Parameters + | "PointerToDecl" | "pointertodecl" -> "PointerToDecl", Some CTL.PointerToDecl + | _ -> "None", None } ; formula_EF: @@ -210,22 +210,28 @@ formula: | formula_id { CTL.Atomic($1, []) } | atomic_formula { Logging.out "\tParsed atomic formula\n"; $1 } | formula EU formula { Logging.out "\tParsed EU\n"; CTL.EU (None, $1, $3) } - | formula AU formula { Logging.out "\tParsed AU\n"; CTL.AU ($1, $3) } - | formula AF { Logging.out "\tParsed AF\n"; CTL.AF ($1) } + | formula AU formula { Logging.out "\tParsed AU\n"; CTL.AU (None,$1, $3) } + | formula AF { Logging.out "\tParsed AF\n"; CTL.AF (None,$1) } | formula EX { Logging.out "\tParsed EX\n"; CTL.EX (None, $1) } - | formula AX { Logging.out "\tParsed AX\n"; CTL.AX ($1) } + | formula AX { Logging.out "\tParsed AX\n"; CTL.AX (None, $1) } | formula EG { Logging.out "\tParsed EG\n"; CTL.EG (None, $1) } - | formula AG { Logging.out "\tParsed AG\n"; CTL.AG ($1) } + | formula AG { Logging.out "\tParsed AG\n"; CTL.AG (None, $1) } | formula EH node_list { Logging.out "\tParsed EH\n"; CTL.EH ($3, $1) } | formula EF { Logging.out "\tParsed EF\n"; CTL.EF (None, $1) } | WHEN formula HOLDS_IN_NODE node_list { Logging.out "\tParsed InNode\n"; CTL.InNode ($4, $2)} | ET node_list WITH_TRANSITION transition_label formula_EF - { Logging.out "\tParsed ET\n"; CTL.ET ($2, $4, $5)} + { Logging.out "\tParsed ET with transition '%s'\n" (fst $4); + CTL.ET ($2, snd $4, $5)} | ETX node_list WITH_TRANSITION transition_label formula_EF - { Logging.out "\tParsed ETX\n"; CTL.ETX ($2, $4, $5)} + { Logging.out "\tParsed ETX ith transition '%s'\n" (fst $4); + CTL.ETX ($2, snd $4, $5)} | EX WITH_TRANSITION transition_label formula_with_paren - { Logging.out "\tParsed EX\n"; CTL.EX ($3, $4)} + { Logging.out "\tParsed EX with transition '%s'\n" (fst $3); + CTL.EX (snd $3, $4)} + | AX WITH_TRANSITION transition_label formula_with_paren + { Logging.out "\tParsed AX with transition '%s'\n" (fst $3); + CTL.AX (snd $3, $4)} | formula AND formula { Logging.out "\tParsed AND\n"; CTL.And ($1, $3) } | formula OR formula { Logging.out "\tParsed OR\n"; CTL.Or ($1, $3) } | formula IMPLIES formula { Logging.out "\tParsed IMPLIES\n"; CTL.Implies ($1, $3) } diff --git a/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp b/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp index 63e44252e..c0198778e 100644 --- a/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp +++ b/infer/tests/codetoanalyze/objc/linters-for-test-only/issues.exp @@ -3,8 +3,10 @@ codetoanalyze/objc/linters-for-test-only/implicit_cast.c, main, 11, TEST_IMPLICI codetoanalyze/objc/linters-for-test-only/implicit_cast.c, main, 11, TEST_VAR_TYPE_CHECK, [] codetoanalyze/objc/linters-for-test-only/namespace.mm, Linters_dummy_method, 9, TEST_NAMESPACE_NAME, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, A_foo:, 13, TEST_BUILTIN_TYPE, [] +codetoanalyze/objc/linters-for-test-only/subclassing.m, A_foo:, 13, TEST_PARAM_TYPE_CHECK2, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, A_foo:, 13, TEST_RETURN_METHOD, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, A_foo:, 19, TEST_BUILTIN_TYPE, [] +codetoanalyze/objc/linters-for-test-only/subclassing.m, A_foo:, 19, TEST_PARAM_TYPE_CHECK2, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, A_foo:, 19, TEST_RETURN_METHOD, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, B_bar, 28, TEST_BUILTIN_TYPE, [] codetoanalyze/objc/linters-for-test-only/subclassing.m, B_bar, 28, TEST_RETURN_METHOD, [] diff --git a/infer/tests/codetoanalyze/objc/linters-for-test-only/linters_example.al b/infer/tests/codetoanalyze/objc/linters-for-test-only/linters_example.al index 4fd97d603..1a0d91436 100644 --- a/infer/tests/codetoanalyze/objc/linters-for-test-only/linters_example.al +++ b/infer/tests/codetoanalyze/objc/linters-for-test-only/linters_example.al @@ -15,6 +15,18 @@ GLOBAL-MACROS { HOLDS-NEXT WITH-TRANSITION Parameters (has_type(x)) HOLDS-IN-NODE ObjCMethodDecl; + + LET method_has_at_least_a_parameter = + WHEN + HOLDS-NEXT WITH-TRANSITION Parameters + (TRUE) + HOLDS-IN-NODE ObjCMethodDecl; + + LET method_has_all_parameter_with_type(x) = + WHEN + HOLDS-EVERYWHERE-NEXT WITH-TRANSITION Parameters + (has_type(x)) + HOLDS-IN-NODE ObjCMethodDecl; }; @@ -173,6 +185,15 @@ DEFINE-CHECKER TEST_PARAM_TYPE_CHECK = { }; +DEFINE-CHECKER TEST_PARAM_TYPE_CHECK2 = { + + SET report_when = method_has_at_least_a_parameter AND + method_has_all_parameter_with_type("int"); + + SET message = "Found a method with a parameter of type...."; + +}; + DEFINE-CHECKER TEST_NTH_PARAM_TYPE_CHECK = { SET report_when =