diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index f62f0a71dd5..51421075c5a 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -2146,7 +2146,7 @@ let add_missed_captures missed_captures ({transitive_info} as astate) = let add_recursive_call location callee astate = let trace = PulseMutualRecursion.mk location callee in let recursive_calls = PulseMutualRecursion.Set.add trace astate.recursive_calls in - ({astate with recursive_calls}, trace) + {astate with recursive_calls} let add_recursive_calls traces astate = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 9ba12231be1..19cb9f49648 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -321,7 +321,7 @@ val finalize_all_hack_builders : t -> t val mark_potential_leaks : Location.t -> dead_roots:Var.t list -> t -> t -val add_recursive_call : Location.t -> Procname.t -> t -> t * PulseMutualRecursion.t +val add_recursive_call : Location.t -> Procname.t -> t -> t val add_recursive_calls : PulseMutualRecursion.Set.t -> t -> t diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index 4e8599c7398..735f0ac259e 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -633,11 +633,12 @@ let maybe_dynamic_type_specialization_is_needed already_specialized contradictio let on_recursive_call ({InterproceduralAnalysis.proc_desc} as analysis_data) call_loc callee_pname astate = - let astate, cycle = AbductiveDomain.add_recursive_call call_loc callee_pname astate in - if Procname.equal callee_pname (Procdesc.get_proc_name proc_desc) then + if Procname.equal callee_pname (Procdesc.get_proc_name proc_desc) then ( PulseReport.report analysis_data ~is_suppressed:false ~latent:false - (MutualRecursionCycle {cycle; location= call_loc}) ; - astate + (MutualRecursionCycle + {cycle= PulseMutualRecursion.mk call_loc callee_pname; location= call_loc} ) ; + astate ) + else AbductiveDomain.add_recursive_call call_loc callee_pname astate let check_uninit_method ({InterproceduralAnalysis.tenv} as analysis_data) call_loc callee_pname diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index e56f40be34c..921d97aaa8c 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -963,24 +963,22 @@ let report_mutual_recursion_cycle if is_foreign_procedure then add_errlog inner_call err_log ) -let report_recursive_calls ({InterproceduralAnalysis.proc_desc} as analysis_data) cycles = - PulseMutualRecursion.Set.iter - (fun cycle -> - if - Procname.equal - (PulseMutualRecursion.get_inner_call cycle) - (Procdesc.get_proc_name proc_desc) - then report_mutual_recursion_cycle analysis_data cycle ) - cycles - - -let record_recursive_calls analysis_data callee_proc_name call_loc callee_summary call_state = +let record_recursive_calls ({InterproceduralAnalysis.proc_desc} as analysis_data) callee_proc_name + call_loc callee_summary call_state = let callee_recursive_calls = - PulseMutualRecursion.Set.map - (PulseMutualRecursion.add_call callee_proc_name call_loc) + PulseMutualRecursion.Set.filter_map + (fun cycle -> + let cycle = PulseMutualRecursion.add_call callee_proc_name call_loc cycle in + if + Procname.equal + (PulseMutualRecursion.get_inner_call cycle) + (Procdesc.get_proc_name proc_desc) + then ( + report_mutual_recursion_cycle analysis_data cycle ; + None ) + else Some cycle ) (AbductiveDomain.Summary.get_recursive_calls callee_summary) in - report_recursive_calls analysis_data callee_recursive_calls ; let astate = AbductiveDomain.add_recursive_calls callee_recursive_calls call_state.astate in {call_state with astate} diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index ac3df9860c1..7d6e2935cdd 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -180,7 +180,6 @@ codetoanalyze/c/pulse/specialization.c, add_more_bad, 2, MUTUAL_RECURSION_CYCLE, codetoanalyze/c/pulse/specialization.c, test_invoke_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/specialization.c, test_recursive_invoke_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/specialization.c, two_pointers_recursion_bad, 2, MUTUAL_RECURSION_CYCLE, no_bucket, WARNING, [`two_pointers_recursion_bad` makes a recursive call to `two_pointers_recursion_bad`] -codetoanalyze/c/pulse/specialization.c, invoke_itself_bad, 3, MUTUAL_RECURSION_CYCLE, no_bucket, WARNING, [`invoke_itself_bad` calls `invoke_itself_bad`,`invoke_itself_bad` makes a recursive call to `invoke_itself_bad`] codetoanalyze/c/pulse/specialization.c, invoke_itself_bad, 3, MUTUAL_RECURSION_CYCLE, no_bucket, WARNING, [`invoke_itself_bad` makes a recursive call to `invoke_itself_bad`] codetoanalyze/c/pulse/taint_var_arg.c, printf_source_bad1, 0, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `int_source` with kind `Simple`,flows to this sink: value passed as argument `#2` to `printf` with kind `Simple`], source: int_source, sink: printf, tainted expression: int_source() codetoanalyze/c/pulse/taint_var_arg.c, printf_source_bad2, 1, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `int_source` with kind `Simple`,flows to this sink: value passed as argument `#2` to `printf` with kind `Simple`], source: int_source, sink: printf, tainted expression: int_source()