From 622366269d429622fe563adc8ef86d9270997125 Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Fri, 28 Oct 2016 04:03:15 -0700 Subject: [PATCH] Simplified semantics of ET and EH Reviewed By: dulmarod Differential Revision: D4074176 fbshipit-source-id: 8e8a6ef --- infer/src/clang/cFrontend_checkers.ml | 12 +- infer/src/clang/cTL.ml | 254 ++++++++++-------- infer/src/clang/cTL.mli | 24 +- infer/src/clang/ctl_parser.mly | 8 +- .../linters/registered_observer/param-block.m | 47 ++++ 5 files changed, 205 insertions(+), 140 deletions(-) create mode 100644 infer/tests/codetoanalyze/objc/linters/registered_observer/param-block.m diff --git a/infer/src/clang/cFrontend_checkers.ml b/infer/src/clang/cFrontend_checkers.ml index 87957e880..2f681725a 100644 --- a/infer/src/clang/cFrontend_checkers.ml +++ b/infer/src/clang/cFrontend_checkers.ml @@ -79,16 +79,16 @@ let ctl_makes_an_expensive_call () = let ctl_ns_notification lctx decl = let open CTL in let exists_method_calling_addObserver = - EF (Atomic ("call_method", ["addObserver:selector:name:object:"])) in + EF (None, (Atomic ("call_method", ["addObserver:selector:name:object:"]))) in let exists_method_calling_addObserverForName = - EF (Atomic ("call_method", ["addObserverForName:object:queue:usingBlock:"])) in + EF (None, (Atomic ("call_method", ["addObserverForName:object:queue:usingBlock:"]))) in let add_observer = Or (exists_method_calling_addObserver, exists_method_calling_addObserverForName) in let eventually_addObserver = ET(["ObjCMethodDecl"], Some Body, add_observer) in let exists_method_calling_removeObserver = - EF(Atomic ("call_method",["removeObserver:"])) in + EF (None, (Atomic ("call_method",["removeObserver:"]))) in let exists_method_calling_removeObserverName = - EF(Atomic ("call_method",["removeObserver:name:object:"])) in + EF (None, (Atomic ("call_method",["removeObserver:name:object:"]))) in let remove_observer = Or(exists_method_calling_removeObserver, exists_method_calling_removeObserverName) in let remove_observer_in_block = ET(["BlockDecl"], Some Body, remove_observer) in @@ -128,7 +128,7 @@ let ctl_bad_pointer_comparison_warning lctx stmt = *) let p = Or (is_expr_with_cleanups, Or (is_implicit_cast_expr, Or (is_binop, is_unop_lnot))) in let p' = And (Not is_binop_neq, p) in - let condition = EU (p', is_nsnumber) in + let condition = EU (None, p', is_nsnumber) in let issue_desc = { CIssue. issue = CIssue.Bad_pointer_comparison; @@ -171,7 +171,7 @@ let ctl_global_var_init_with_calls_warning lctx decl = And (And (Atomic ("is_objc_extension", []), Atomic ("is_global_var", [])), Not (Atomic ("is_const_var", []))) in let ctl_is_initialized_with_expensive_call = - ET(["VarDecl"], Some InitExpr, EF (ctl_makes_an_expensive_call ())) in + ET(["VarDecl"], Some InitExpr, EF (None, (ctl_makes_an_expensive_call ()))) in let condition = And (ctl_is_global_var, ctl_is_initialized_with_expensive_call) in let issue_desc = { CIssue.issue = CIssue.Global_variable_initialized_with_function_or_method_call; diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 4b64928ed..41f7565db 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -17,10 +17,11 @@ open CFrontend_utils report a problem *) -(* Label that allows switching from a decl node to a stmt node *) -type transition_decl_to_stmt = - | Body - | InitExpr +(* Transition labels used for example to switch from decl to stmt *) +type transitions = + | Body (* decl to stmt *) + | InitExpr (* decl to stmt *) + | Super (* decl to decl *) (* In formulas below prefix "E" means "exists a path" @@ -34,16 +35,17 @@ type t = (* A ctl formula *) | And of t * t | Or of t * t | Implies of t * t + | InNode of string list * t | AX of t - | EX of t + | EX of transitions option * t | AF of t - | EF of t + | EF of transitions option * t | AG of t - | EG of t + | EG of transitions option * t | AU of t * t - | EU of t * t + | EU of transitions option * t * t | EH of string list * t - | ET of string list * transition_decl_to_stmt option * t + | ET of string list * transitions option * t (* the kind of AST nodes where formulas are evaluated *) type ast_node = @@ -51,13 +53,14 @@ type ast_node = | Decl of Clang_ast_t.decl module Debug = struct - let pp_transition_decl_to_stmt fmt trans_opt = + let pp_transition fmt trans_opt = let pp_aux fmt trans = match trans with | Body -> Format.pp_print_string fmt "Body" - | InitExpr -> Format.pp_print_string fmt "InitExpr" in + | InitExpr -> Format.pp_print_string fmt "InitExpr" + | Super -> Format.pp_print_string fmt "Super" in match trans_opt with | Some trans -> pp_aux fmt trans - | None -> Format.pp_print_string fmt "None" + | None -> Format.pp_print_string fmt "_" let rec pp_formula fmt phi = match phi with @@ -68,20 +71,24 @@ module Debug = struct | And (phi1, phi2) -> Format.fprintf fmt "(%a AND %a)" pp_formula phi1 pp_formula phi2 | Or (phi1, phi2) -> Format.fprintf fmt "(%a OR %a)" pp_formula phi1 pp_formula phi2 | Implies (phi1, phi2) -> Format.fprintf fmt "(%a ==> %a)" pp_formula phi1 pp_formula phi2 + | InNode (nl, phi) -> Format.fprintf fmt "IN-NODE %a: (%a)" + (Utils.pp_comma_seq Format.pp_print_string) nl + pp_formula phi | AX phi -> Format.fprintf fmt "AX(%a)" pp_formula phi - | EX phi -> Format.fprintf fmt "EX(%a)" 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 - | EF phi -> Format.fprintf fmt "EF(%a)" 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 - | EG phi -> Format.fprintf fmt "EG(%a)" 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 - | EU (phi1, phi2) -> Format.fprintf fmt "E[%a UNTIL %a]" 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)" (Utils.pp_comma_seq Format.pp_print_string) arglist pp_formula phi | ET (arglist, trans, phi) -> Format.fprintf fmt "ET[%a][%a](%a)" (Utils.pp_comma_seq Format.pp_print_string) arglist - pp_transition_decl_to_stmt trans + pp_transition trans pp_formula phi module EvaluationTracker = struct @@ -235,44 +242,69 @@ let save_dotty_when_in_debug_mode source_file = (* Helper functions *) +(* Sometimes we need to unwrap a node *) +(* NOTE: when in the language it will be possible to define + sintactic sugar than we can remove this and define it a + transition from BlockExpr to BlockDecl *) +let unwrap_node an = + match an with + | Stmt BlockExpr(_, _, _, d) -> + (* From BlockExpr we jump directly to its BlockDecl *) + Decl d + | _ -> an + +let node_to_string an = + match an with + | Decl d -> Clang_ast_proj.get_decl_kind_string d + | Stmt s -> Clang_ast_proj.get_stmt_kind_string s + (* true iff an ast node is a node of type among the list tl *) let node_has_type tl an = - let an_str = match an with - | Decl d -> Clang_ast_proj.get_decl_kind_string d - | Stmt s -> Clang_ast_proj.get_stmt_kind_string s in + let an_str = node_to_string an in IList.mem (string_equal) an_str tl (* given a decl returns a stmt such that decl--->stmt via label trs *) -let transition_from_decl_to_stmt d trs = +let transition_decl_to_stmt d trs = let open Clang_ast_t in - 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 _ -> - assert false (* to be done. Requires extending to lists *) - | Some InitExpr, EnumConstantDecl (_, _, _, ecdi) -> ecdi.ecdi_init_expr - | _, _ -> None - -(* given a stmt returns a decl such that stmt--->decl via label trs - NOTE: for the moment we don't have any transitions stmt to decl as - we don't have much experience. - TBD: the list need to be populated when we know what we need *) -let transition_from_stmt_to_decl st trs = - match trs, st with - | _, _ -> None (* For the moment always no transitions. TBD add transitions *) + 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 _ -> + assert false (* to be done. Requires extending to lists *) + | Some InitExpr, EnumConstantDecl (_, _, _, ecdi) -> ecdi.ecdi_init_expr + | _, _ -> None in + match temp_res with + | Some st -> Some (Stmt st) + | _ -> None + +let transition_decl_to_decl_via_super d = + match Ast_utils.get_impl_decl_info d with + | Some idi -> + (match Ast_utils.get_super_ObjCImplementationDecl idi with + | Some d -> Some (Decl d) + | _ -> None) + | None -> None +(* given a node an returns the node 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 InitExpr + | Decl d, Some Body -> transition_decl_to_stmt d trans + | _, _ -> None (* Evaluation of formulas *) @@ -311,10 +343,10 @@ let eval_Atomic pred_name params an lcxt = either (st,lcxt) satifies phi or there is a child st' of the node st such that (st', lcxt) satifies EF phi *) -let rec eval_EF_st phi st lcxt = +let rec eval_EF_st phi st lcxt trans = let _, succs = Clang_ast_proj.get_stmt_tuple st in eval_formula phi (Stmt st) lcxt - || IList.exists (fun s -> eval_EF phi (Stmt s) lcxt) succs + || IList.exists (fun s -> eval_EF phi (Stmt s) lcxt trans) succs (* dec, lcxt |= EF phi <=> @@ -322,18 +354,22 @@ let rec eval_EF_st phi st lcxt = This is as eval_EF_st but for decl. *) -and eval_EF_decl phi dec lcxt = +and eval_EF_decl phi dec lcxt trans = eval_formula phi (Decl dec) lcxt || (match Clang_ast_proj.get_decl_context_tuple dec with | Some (decl_list, _) -> - IList.exists (fun d -> eval_EF phi (Decl d) lcxt) decl_list + IList.exists (fun d -> eval_EF phi (Decl d) lcxt trans) decl_list | None -> false) (* an, lcxt |= EF phi evaluates on decl or stmt depending on an *) -and eval_EF phi an lcxt = - match an with - | Stmt st -> eval_EF_st phi st lcxt - | Decl dec -> eval_EF_decl phi dec lcxt +and eval_EF phi an lcxt trans = + match trans, an with + | Some _, _ -> + (* Using equivalence EF[->trans] phi = phi OR EX[->trans](EF[->trans] phi)*) + let phi' = Or (phi, EX (trans, EF (trans, phi))) in + eval_formula phi' an lcxt + | None, Stmt st -> eval_EF_st phi st lcxt trans + | None, Decl dec -> eval_EF_decl phi dec lcxt trans (* st, lcxt |= EX phi <=> exists st' in Successors(st): st', lcxt |= phi @@ -355,11 +391,19 @@ and eval_EX_decl phi dec lcxt = IList.exists (fun d -> eval_formula phi (Decl d) lcxt) decl_list | None -> false +(* Evaluate phi on node an' such that an -l-> an'. False if an' does not exists *) +and evaluate_on_transition phi an lcxt l = + match next_state_via_transition an l with + | Some succ -> eval_formula phi succ lcxt + | None -> false + (* an |= EX phi evaluates on decl/stmt depending on the ast_node an *) -and eval_EX phi an lcxt = - match an with - | Stmt st -> eval_EX_st phi st lcxt - | Decl decl -> eval_EX_decl phi decl lcxt +and eval_EX phi an lcxt trans = + match trans, an with + | Some _, _ -> evaluate_on_transition phi an lcxt trans + | None, Stmt st -> eval_EX_st phi st lcxt + | None, Decl decl -> eval_EX_decl phi decl lcxt + (* 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))) @@ -367,8 +411,8 @@ and eval_EX phi an lcxt = That is: a (an,lcxt) satifies E(phi1 U phi2) if and only if an,lcxt satifies the formula phi2 or (phi1 and EX(E(phi1 U phi2))) *) -and eval_EU phi1 phi2 an lcxt = - let f = Or (phi2, And (phi1, EX (EU (phi1, phi2)))) in +and eval_EU phi1 phi2 an lcxt trans = + let f = Or (phi2, And (phi1, EX (trans, (EU (trans, phi1, phi2))))) in eval_formula f an lcxt (* an |= A(phi1 U phi2) evaluated using the equivalence @@ -380,6 +424,12 @@ and eval_AU phi1 phi2 an lcxt = let f = Or (phi2, And (phi1, AX (AU (phi1, phi2)))) in eval_formula f an lcxt +(* an, lcxt |= InNode[node_type_list] phi <=> + an is a node of type in node_type_list and an satifies phi +*) +and in_node node_type_list phi an lctx = + (node_has_type node_type_list an) && (eval_formula phi an lctx) + (* Intuitive meaning: (an,lcxt) satifies EH[Classes] phi if the node an is among the declaration specified by the list Classes and there exists a super class in its hierarchy whose declaration satisfy phi. @@ -388,62 +438,25 @@ and eval_AU phi1 phi2 an lcxt = the node an is in Classes and there exists a declaration d in Hierarchy(an) such that d,lcxt |= phi *) and eval_EH classes phi an lcxt = - let rec eval_super impl_decl_info = - match impl_decl_info with - | Some idi -> - (match Ast_utils.get_super_ObjCImplementationDecl idi with - | Some (Clang_ast_t.ObjCImplementationDecl(_, _, _, _, idi') as d) -> - eval_formula phi (Decl d) lcxt || eval_super (Some idi') - | _ -> false) - | None -> false in - match an with - | Decl d when node_has_type classes (Decl d) -> - eval_super (Ast_utils.get_impl_decl_info d) - | _ -> false + (* Define EH[Classes] phi = ET[Classes](EF[->Super] phi) *) + let f = ET (classes, None, EF (Some Super, phi)) in + eval_formula f an lcxt (* an, lcxt |= ET[T][->l]phi <=> - an is a node among those defined in T and an-l->an' - ("an transitions" to another node an' via an edge labelled l) - such that an',lcxt |= phi + eventually we reach a node an' such that an' is among the types defined in T + and: - or an is a node among those defined in T, and l is unspecified, - and an,lcxt |= phi + an'-l->an'' + ("an' transitions" to another node an'' via an edge labelled l) + and an'',lcxt |= phi - or an is not of type in T and exists an' in Successors(an): - an', lcxt |= ET[T][->l]phi + or l is unspecified and an,lcxt |= phi *) and eval_ET tl trs phi an lcxt = - let open Clang_ast_t in - let evaluate_on_subdeclarations d eval = - match Clang_ast_proj.get_decl_context_tuple d with - | None -> false - | Some (decl_list, _) -> - IList.exists (fun d' -> eval phi (Decl d') lcxt) decl_list in - let evaluate_on_substmt st eval = - let _, stmt_list = Clang_ast_proj.get_stmt_tuple st in - IList.exists (fun s -> eval phi (Stmt s) lcxt) stmt_list in - let do_decl d = - match trs, node_has_type tl (Decl d) with - | Some _, true -> - (match transition_from_decl_to_stmt d trs with - | None -> false - | Some st -> eval_formula phi (Stmt st) lcxt) - | None, true -> eval_formula phi (Decl d) lcxt - | _, false -> evaluate_on_subdeclarations d (eval_ET tl trs) in - let do_stmt st = - match trs, node_has_type tl (Stmt st) with - | Some _, true -> - (match transition_from_stmt_to_decl st trs with - | None -> false - | Some d -> eval_formula phi (Decl d) lcxt) - | None, true -> eval_formula phi (Stmt st) lcxt - | _, false -> evaluate_on_substmt st (eval_ET tl trs) in - match an with - | Decl d -> do_decl d - | Stmt BlockExpr(_, _, _, d) -> - (* From BlockExpr we jump directly to its BlockDecl *) - eval_ET tl trs phi (Decl d) lcxt - | Stmt st -> do_stmt st + let f = match trs with + | Some _ -> EF (None, (InNode (tl, EX (trs, phi)))) + | None -> EF (None, (InNode (tl, phi))) in + eval_formula f an lcxt (* Formulas are evaluated on a AST node an and a linter context lcxt *) and eval_formula f an lcxt = @@ -457,16 +470,19 @@ and eval_formula f an lcxt = | Or (f1, f2) -> (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt) | Implies (f1, f2) -> not (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt) + | InNode (node_type_list, f1) -> + let an' = unwrap_node an in + in_node node_type_list f1 an' lcxt | AU (f1, f2) -> eval_AU f1 f2 an lcxt - | EU (f1, f2) -> eval_EU f1 f2 an lcxt - | EF f1 -> eval_EF f1 an lcxt + | 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 (Not f1))) an lcxt - | EX f1 -> eval_EX f1 an lcxt - | AX f1 -> eval_formula (Not (EX (Not f1))) an lcxt + | AG f1 -> eval_formula (Not (EF (None, (Not f1)))) an lcxt + | EX (trans, f1) -> eval_EX f1 an lcxt trans + | AX f1 -> eval_formula (Not (EX (None, (Not f1)))) an lcxt | EH (cl, phi) -> eval_EH cl phi an lcxt - | EG f1 -> (* st |= EG f1 <=> st |= f1 /\ EX EG f1 *) - eval_formula (And (f1, EX (EG (f1)))) an lcxt + | EG (trans, f1) -> (* st |= EG f1 <=> st |= f1 /\ EX EG f1 *) + eval_formula (And (f1, EX (trans, (EG (trans, f1))))) an lcxt | ET (tl, sw, phi) -> eval_ET tl sw phi an lcxt in debug_eval_end res; res diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 9da7a884f..bea148926 100644 --- a/infer/src/clang/cTL.mli +++ b/infer/src/clang/cTL.mli @@ -12,10 +12,11 @@ CTL formula which express a condition saying when the checker should report a problem *) -type transition_decl_to_stmt = - | Body - | InitExpr - +(* Transition labels used for example to switch from decl to stmt *) +type transitions = + | Body (* decl to stmt *) + | InitExpr (* decl to stmt *) + | Super (* decl to decl *) (* In formulas below prefix "E" means "exists a path" @@ -30,21 +31,22 @@ type t = | And of t * t | Or of t * t | Implies of t * t + | InNode of string list * t | AX of t (** AX phi <=> for all children of the current node phi holds *) - | EX of t (** EX phi <=> exist a child of the current node such that 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 *) - | EF of t (** EF phi <=> there exits a a path from the current node with a descendant where phi hold *) + | 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 *) - | EG of t (** EG phi <=> - there exists a path (of descendants) from the current node where phi hold at each node of the path *) + | 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 *) - | EU of t * t (** EU(phi1, phi2) <=> - there exists a path from the current node such that phi1 holds until phi2 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 string list * t (** EH[classes]phi <=> there exists a node defining a super class in the hierarchy of the class defined by the current node (if any) where phi holds *) - | ET of string list * transition_decl_to_stmt option * t (** ET[T][l] phi <=> + | ET of string list * transitions option * t (** ET[T][l] phi <=> there exists a descentant an of the current node such that an is of type in set T making a transition to a node an' via label l, such that in an phi holds. *) diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index e655fd677..c2ce87f00 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/infer/src/clang/ctl_parser.mly @@ -109,15 +109,15 @@ formula: | LEFT_PAREN formula RIGHT_PAREN { $2 } | formula_id { $1 } | atomic_formula { Logging.out "\tParsed atomic formula\n"; $1 } - | formula EU formula { Logging.out "\tParsed EU\n"; CTL.EU ($1, $3) } + | 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 EX { Logging.out "\tParsed EX\n"; CTL.EX ($1) } + | formula EX { Logging.out "\tParsed EX\n"; CTL.EX (None, $1) } | formula AX { Logging.out "\tParsed AX\n"; CTL.AX ($1) } - | formula EG { Logging.out "\tParsed EG\n"; CTL.EG ($1) } + | formula EG { Logging.out "\tParsed EG\n"; CTL.EG (None, $1) } | formula AG { Logging.out "\tParsed AG\n"; CTL.AG ($1) } | formula EH params { Logging.out "\tParsed EH\n"; CTL.EH ($3, $1) } - | formula EF { Logging.out "\tParsed EF\n"; CTL.EF ($1) } + | formula EF { Logging.out "\tParsed EF\n"; CTL.EF (None, $1) } | ET params WITH_TRANSITION transition_label formula_EF { Logging.out "\tParsed ET\n"; CTL.ET ($2, $4, $5)} | formula AND formula { Logging.out "\tParsed AND\n"; CTL.And ($1, $3) } diff --git a/infer/tests/codetoanalyze/objc/linters/registered_observer/param-block.m b/infer/tests/codetoanalyze/objc/linters/registered_observer/param-block.m new file mode 100644 index 000000000..25075eae3 --- /dev/null +++ b/infer/tests/codetoanalyze/objc/linters/registered_observer/param-block.m @@ -0,0 +1,47 @@ +/* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +#import + +@interface AA : NSObject + +@property(strong) NSNotificationCenter* nc; + +- (void)my_method:(double)d + block_param:(double (^)(double time))myblock + st:(int)numSteps; + +@end + +@implementation AA + +- (void)foo { + [self.nc addObserver:self selector:@selector(foo:) name:nil object:nil]; +} + +- (void)my_method:(double)d + block_param:(double (^)(double time))myblock + st:(int)num { + for (int i = 1; i <= num; i++) { + if (myblock) + myblock(i * d * num); + } +} + +- (void)boo { + + [self my_method:5.3 + block_param:^(double time) { + [self.nc removeObserver:self]; + return time + 7.4; + } + st:30]; +} + +@end