From e1093159b05848d3709cbfa1fde5a7262194e401 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 9 Apr 2020 05:49:20 -0700 Subject: [PATCH] [pulse] Distinguish error state at top level Summary: As soon as pulse detects an error, it completely stops the analysis and loses the state where the error occurred. This makes it difficult to debug and understand the state the program failed. Moreover, other analyses that might build on pulse (e.g. impurity), cannot access the error state. This diff aims to restore and display the state at the time of the error in `PulseExecutionState` along with the diagnostic by extending it as follows: ``` type exec_state = | represents the state at the program point that caused an error *) ``` As a result, since we don't immediately stop the analysis as soon as we find an error, we detect both errors in conditional branches simultaneously (see test result changes for examples). NOTE: We need to extend `PulseOperations.access_result` to keep track of the failed state as follows: ``` type 'a access_result = ('a, Diagnostic.t * t [denoting the exit state] ) result ``` Reviewed By: jvillard Differential Revision: D20918920 fbshipit-source-id: 432ac68d6 --- infer/src/absint/AbstractDomain.ml | 2 - infer/src/absint/AbstractDomain.mli | 4 -- infer/src/absint/AbstractInterpreter.ml | 2 - infer/src/checkers/impurity.ml | 2 +- infer/src/pulse/Pulse.ml | 47 ++++++++++--------- infer/src/pulse/PulseAbductiveDomain.ml | 5 +- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseExecutionState.ml | 11 ++++- infer/src/pulse/PulseExecutionState.mli | 2 + infer/src/pulse/PulseOperations.ml | 24 ++++++---- infer/src/pulse/PulseOperations.mli | 4 +- .../codetoanalyze/cpp/impurity/issues.exp | 2 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 2 + 13 files changed, 60 insertions(+), 49 deletions(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 69fa1c11c..2af92120d 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -18,8 +18,6 @@ end open! Types -exception Stop_analysis - module type NoJoin = sig include PrettyPrintable.PrintableType diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 218770ec2..9cb4543b0 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -17,10 +17,6 @@ end open! Types -exception Stop_analysis -(** This exception can be raised by abstract interpreters to stop the analysis early without - triggering further errors. Clients who raise this exception should catch it eventually. *) - (** Abstract domains and domain combinators *) module type NoJoin = sig diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index ffdd5a03b..fef307f2a 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -179,8 +179,6 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s match post with | Ok astate_post -> InvariantMap.add node_id {State.pre; post= astate_post; visit_count} inv_map - | Error (AbstractDomain.Stop_analysis, _, _) -> - raise_notrace AbstractDomain.Stop_analysis | Error (exn, backtrace, instr) -> if not !logged_error then ( L.internal_error "In instruction %a@\n" (Sil.pp_instr ~print_types:true Pp.text) instr ; diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 01e38fc80..35407e10d 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -143,7 +143,7 @@ let extract_impurity tenv pdesc (exec_state : PulseExecutionState.t) : ImpurityD match exec_state with | ExitProgram astate -> (astate, true) - | ContinueProgram astate -> + | AbortProgram astate | ContinueProgram astate -> (astate, false) in let pre_heap = (PulseAbductiveDomain.get_pre astate).BaseDomain.heap in diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 2075ad407..16111c691 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -17,18 +17,18 @@ let report summary diagnostic = (get_issue_type diagnostic) (get_message diagnostic) -let check_error summary = function - | Ok ok -> - ok - | Error diagnostic -> +let check_error_transform summary ~f = function + | Ok astate -> + f astate + | Error (diagnostic, astate) -> report summary diagnostic ; - (* We can also continue the analysis by returning {!PulseDomain.initial} here but there might - be a risk we would get nonsense. This seems safer for now but TODO. *) - raise_notrace AbstractDomain.Stop_analysis + [PulseExecutionState.AbortProgram astate] let check_error_continue summary result = - PulseExecutionState.ContinueProgram (check_error summary result) + check_error_transform summary + ~f:(fun astate -> [PulseExecutionState.ContinueProgram astate]) + result let proc_name_of_call call_exp = @@ -82,7 +82,7 @@ module PulseTransferFunctions = struct (* invalidate [&x] *) PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate >>| PulseExecutionState.continue - | PulseExecutionState.ExitProgram _ -> + | PulseExecutionState.AbortProgram _ | PulseExecutionState.ExitProgram _ -> Ok exec_state @@ -141,6 +141,10 @@ module PulseTransferFunctions = struct let exec_instr (astate : Domain.t) {tenv; ProcData.summary; extras= get_formals} _cfg_node (instr : Sil.instr) : Domain.t list = match astate with + | AbortProgram _ -> + (* We can also continue the analysis with the error state here + but there might be a risk we would get nonsense. *) + [astate] | ExitProgram _ -> (* program already exited, simply propagate the exited state upwards *) [astate] @@ -152,7 +156,7 @@ module PulseTransferFunctions = struct let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in PulseOperations.write_id lhs_id rhs_addr_hist astate in - [check_error_continue summary result] + check_error_continue summary result | Store {e1= lhs_exp; e2= rhs_exp; loc} -> (* [*lhs_exp := rhs_exp] *) let event = ValueHistory.Assignment loc in @@ -171,22 +175,21 @@ module PulseTransferFunctions = struct | _ -> Ok astate in - [check_error_continue summary result] + check_error_continue summary result | Prune (condition, loc, is_then_branch, if_kind) -> - let exec_state, cond_satisfiable = - PulseOperations.prune ~is_then_branch if_kind loc ~condition astate - |> check_error summary - in - if cond_satisfiable then - (* [condition] is true or unknown value: go into the branch *) - [Domain.continue exec_state] - else (* [condition] is known to be unsatisfiable: prune path *) [] + PulseOperations.prune ~is_then_branch if_kind loc ~condition astate + |> check_error_transform summary ~f:(fun (exec_state, cond_satisfiable) -> + if cond_satisfiable then + (* [condition] is true or unknown value: go into the branch *) + [Domain.ContinueProgram exec_state] + else (* [condition] is known to be unsatisfiable: prune path *) + [] ) | Call (ret, call_exp, actuals, loc, call_flags) -> dispatch_call tenv summary ret call_exp actuals loc call_flags get_formals astate - |> check_error summary + |> check_error_transform summary ~f:(fun id -> id) | Metadata (ExitScope (vars, location)) -> let astate = PulseOperations.remove_vars vars location astate in - [check_error_continue summary astate] + check_error_continue summary astate | Metadata (VariableLifetimeBegins (pvar, _, location)) -> [PulseOperations.realloc_pvar pvar location astate |> Domain.continue] | Metadata (Abstract _ | Nullify _ | Skip) -> @@ -227,5 +230,3 @@ let checker {Callbacks.exe_env; summary} = summary | None -> summary - | exception AbstractDomain.Stop_analysis -> - summary diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 610a7beb6..d723bb1df 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -1023,8 +1023,9 @@ let check_all_valid callee_proc_name call_location {pre; post= _} call_state = AddressAttributes.check_valid access_trace addr_caller astate |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; - Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} - ) ) ) + ( Diagnostic.AccessToInvalidAddress + {invalidation; invalidation_trace; access_trace} + , astate ) ) ) ) call_state.subst (Ok call_state.astate) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 542103178..6096461f2 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -129,6 +129,6 @@ val apply : -> formals:Var.t list -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> t - -> ((t * (AbstractValue.t * ValueHistory.t) option) option, Diagnostic.t) result + -> ((t * (AbstractValue.t * ValueHistory.t) option) option, Diagnostic.t * t) result (** return the abstract state after the call along with an optional return value, or [None] if the precondition could not be satisfied (e.g. some aliasing constraints were not satisfied) *) diff --git a/infer/src/pulse/PulseExecutionState.ml b/infer/src/pulse/PulseExecutionState.ml index 877451446..68f1ac0d0 100644 --- a/infer/src/pulse/PulseExecutionState.ml +++ b/infer/src/pulse/PulseExecutionState.ml @@ -8,6 +8,7 @@ open! IStd module F = Format type exec_state = + | AbortProgram of PulseAbductiveDomain.t | ContinueProgram of PulseAbductiveDomain.t | ExitProgram of PulseAbductiveDomain.t @@ -19,9 +20,11 @@ let mk_initial pdesc = ContinueProgram (PulseAbductiveDomain.mk_initial pdesc) let leq ~lhs ~rhs = match (lhs, rhs) with - | ContinueProgram astate1, ContinueProgram astate2 | ExitProgram astate1, ExitProgram astate2 -> + | AbortProgram astate1, AbortProgram astate2 + | ContinueProgram astate1, ContinueProgram astate2 + | ExitProgram astate1, ExitProgram astate2 -> PulseAbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 - | ExitProgram _, ContinueProgram _ | ContinueProgram _, ExitProgram _ -> + | _ -> false @@ -30,10 +33,14 @@ let pp fmt = function PulseAbductiveDomain.pp fmt astate | ExitProgram astate -> F.fprintf fmt "{ExitProgram %a}" PulseAbductiveDomain.pp astate + | AbortProgram astate -> + F.fprintf fmt "{AbortProgram %a}" PulseAbductiveDomain.pp astate let map ~f exec_state = match exec_state with + | AbortProgram astate -> + AbortProgram (f astate) | ContinueProgram astate -> ContinueProgram (f astate) | ExitProgram astate -> diff --git a/infer/src/pulse/PulseExecutionState.mli b/infer/src/pulse/PulseExecutionState.mli index 6702e1f8c..0d7e38518 100644 --- a/infer/src/pulse/PulseExecutionState.mli +++ b/infer/src/pulse/PulseExecutionState.mli @@ -7,6 +7,8 @@ open! IStd type exec_state = + | AbortProgram of PulseAbductiveDomain.t + (** represents the state at the program point that caused an error *) | ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *) | ExitProgram of PulseAbductiveDomain.t (** represents the state originating at exit/divergence. *) diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index d87fce623..851cd07ef 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -12,7 +12,7 @@ open PulseDomainInterface type t = AbductiveDomain.t -type 'a access_result = ('a, Diagnostic.t) result +type 'a access_result = ('a, Diagnostic.t * t) result let ok_continue post = Ok [PulseExecutionState.ContinueProgram post] @@ -21,7 +21,8 @@ let check_addr_access location (address, history) astate = let access_trace = Trace.Immediate {location; history} in AddressAttributes.check_valid access_trace address astate |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> - Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} ) + (Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace}, astate) + ) module Closures = struct @@ -439,8 +440,9 @@ let check_address_escape escape_location proc_desc address history astate = (* The returned address corresponds to a C++ temporary. It will have gone out of scope by now except if it was bound to a global. *) Error - (Diagnostic.StackVariableAddressEscape - {variable; location= escape_location; history}) + ( Diagnostic.StackVariableAddressEscape + {variable; location= escape_location; history} + , astate ) | _ -> Ok () ) ) in @@ -457,7 +459,8 @@ let check_address_escape escape_location proc_desc address history astate = L.d_printfln_escaped "Stack variable address &%a detected at address %a" Var.pp variable AbstractValue.pp address ; Error - (Diagnostic.StackVariableAddressEscape {variable; location= escape_location; history}) ) + ( Diagnostic.StackVariableAddressEscape {variable; location= escape_location; history} + , astate ) ) else Ok () ) in let+ () = check_address_of_cpp_temporary () >>= check_address_of_stack_variable in @@ -472,7 +475,7 @@ let mark_address_of_stack_variable history variable location address astate = AddressAttributes.add_one address (AddressOfStackVariable (variable, location, history)) astate -let check_memory_leak_unreachable unreachable_attrs location = +let check_memory_leak_unreachable unreachable_attrs location astate = let check_memory_leak _ attributes result = let allocated_not_freed_opt = Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *)) @@ -488,7 +491,7 @@ let check_memory_leak_unreachable unreachable_attrs location = match allocated_not_freed_opt with | Some (procname, trace), false -> (* allocated but not freed *) - Error (Diagnostic.MemoryLeak {procname; location; allocation_trace= trace}) + Error (Diagnostic.MemoryLeak {procname; location; allocation_trace= trace}, astate) | _ -> result in @@ -515,7 +518,7 @@ let remove_vars vars location astate = if phys_equal astate' astate then Ok astate else let astate, unreachable_attrs = AbductiveDomain.discard_unreachable astate' in - let+ () = check_memory_leak_unreachable unreachable_attrs location in + let+ () = check_memory_leak_unreachable unreachable_attrs location astate in astate @@ -591,6 +594,9 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~formals ~actuals in let open PulseExecutionState in match callee_exec_state with + | AbortProgram _ -> + (* Callee has failed; don't propagate the failure *) + Ok (Some callee_exec_state) | ContinueProgram astate -> apply astate ~f:(fun astate -> ContinueProgram astate) | ExitProgram astate -> @@ -598,7 +604,7 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~formals ~actuals let call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt - (astate : PulseAbductiveDomain.t) : (PulseExecutionState.t list, Diagnostic.t) result = + (astate : PulseAbductiveDomain.t) : (PulseExecutionState.t list, Diagnostic.t * t) result = match PulsePayload.read_full ~caller_summary ~callee_pname with | Some (callee_proc_desc, exec_states) -> let formals = diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index b36099688..bf777ca66 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -11,12 +11,12 @@ open PulseDomainInterface type t = PulseAbductiveDomain.t -type 'a access_result = ('a, Diagnostic.t) result +type 'a access_result = ('a, Diagnostic.t * t) result val ok_continue : t -> (PulseExecutionState.exec_state list, 'a) result module Closures : sig - val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t) result + val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t * t) result (** assert the validity of the addresses captured by the lambda *) end diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index 6375675f4..8650093bc 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -16,7 +16,7 @@ codetoanalyze/cpp/impurity/global_test.cpp, modify_global_inside_lamda_impure::l codetoanalyze/cpp/impurity/global_test.cpp, modify_global_primitive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_primitive_impure,global variable `x` modified here] codetoanalyze/cpp/impurity/invalid_test.cpp, Simple::operator=, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Simple::operator=,parameter `this` modified here] codetoanalyze/cpp/impurity/invalid_test.cpp, delete_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function delete_param_impure,parameter `s` was invalidated by `delete` here] -codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double_free_global_impure with no pulse summary] +codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double_free_global_impure,when calling `free_global_pointer_impure` here,global variable `global_pointer` was invalidated by call to `free()` here] codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_impure` here,global variable `global_pointer` accessed here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_impure` here,global variable `global_pointer` accessed here,invalid access occurs here] codetoanalyze/cpp/impurity/invalid_test.cpp, free_global_pointer_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_global_pointer_impure,global variable `global_pointer` was invalidated by call to `free()` here] codetoanalyze/cpp/impurity/invalid_test.cpp, free_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_param_impure,parameter `x` was invalidated by call to `free()` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 2524c1849..fd949627e 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,5 +1,6 @@ codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `setLanguage` here,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] @@ -22,6 +23,7 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/memory_leak.cpp, constant_index_no_leak_FP, 3, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/cpp/pulse/nullptr.cpp, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]