diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 070543888..9d8786ece 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/infer/src/pulse/PulseTopl.ml @@ -433,25 +433,24 @@ let description_of_step_data step_data = let report_errors proc_desc err_log state = - (* TODO(rgrigore): Calling f() that has implementation leads to a large_step followed by a small_step, - which currently results in two trace elements (that look the same to the user). This is confusing. *) let a = Topl.automaton () in - let rec make_trace nesting acc q = + let rec make_trace nesting trace q = match q.last_step with | None -> - acc + trace | Some {step_location; step_predecessor; step_data} -> let description = description_of_step_data step_data in - let acc = - Errlog.make_trace_element nesting step_location description [] - :: - ( match step_data with + let trace = + let trace_element = Errlog.make_trace_element nesting step_location description [] in + match step_data with | SmallStep _ -> - acc + trace_element :: trace + | LargeStep (_, {last_step= None}) -> + trace (* skip trivial large steps (i.e., those with no steps) *) | LargeStep (_, qq) -> - make_trace (nesting + 1) acc qq ) + trace_element :: make_trace (nesting + 1) trace qq in - make_trace nesting acc step_predecessor + make_trace nesting trace step_predecessor in let report_simple_state q = if ToplAutomaton.is_start a q.pre.vertex && ToplAutomaton.is_error a q.post.vertex then diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp b/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp index 1e7649911..46445ec04 100644 --- a/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp @@ -1,2 +1,2 @@ -codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.aBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int CompareArgs.max(int[],int,int),call to int CompareArgs.max(int[],int,int)] -codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int CompareArgs.max(int[],int,int),call to int CompareArgs.max(int[],int,int)] +codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.aBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int CompareArgs.max(int[],int,int)] +codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int CompareArgs.max(int[],int,int)] diff --git a/infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp b/infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp index 13f656a56..af8ff86ba 100644 --- a/infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badA():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to int[] ImmutableArray.getTestArray(),write to array] -codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badABC():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to int[] ImmutableArray.getTestArray(),write to array,call to void ImmutableArray.otherMutateArray(int[])] -codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badB():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to int[] ImmutableArray.getTestArray(),write to array] -codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badC():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to int[] ImmutableArray.getTestArray(),call to void ImmutableArray.otherMutateArray(int[]),write to array] +codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badA():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),write to array] +codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badABC():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),write to array] +codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badB():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),write to array] +codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badC():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to void ImmutableArray.otherMutateArray(int[]),write to array]