[pulse] more details about variable declaration events

Summary:
- add the variable being declared so we can report it back in the trace in addition to its location
- distinguish between local vars and formals

Reviewed By: skcho

Differential Revision: D17930348

fbshipit-source-id: a5b863e64

infer/src/pulse/Pulse.ml

@@ -199,7 +199,7 @@ module PulseTransferFunctions = struct
     | Metadata (ExitScope (vars, location)) ->
         [PulseOperations.remove_vars vars location astate]
     | Metadata (VariableLifetimeBegins (pvar, _, location)) ->
-        [PulseOperations.realloc_var (Var.of_pvar pvar) location astate]
+        [PulseOperations.realloc_pvar pvar location astate]
     | Metadata (Abstract _ | Nullify _ | Skip) ->
         [astate]
 

infer/src/pulse/PulseAbductiveDomain.ml

@@ -239,10 +239,10 @@ let mk_initial proc_desc =
     let location = Procdesc.get_loc proc_desc in
     Procdesc.get_formals proc_desc
     |> List.map ~f:(fun (mangled, _) ->
-           let var = Var.of_pvar (Pvar.mk mangled proc_name) in
-           ( var
-           , (AbstractAddress.mk_fresh (), [PulseDomain.ValueHistory.VariableDeclaration location])
-           ) )
+           let pvar = Pvar.mk mangled proc_name in
+           ( Var.of_pvar pvar
+           , ( AbstractAddress.mk_fresh ()
+             , [PulseDomain.ValueHistory.FormalDeclared (pvar, location)] ) ) )
   in
   let initial_stack =
     List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack

infer/src/pulse/PulseDomain.ml

@@ -127,7 +127,8 @@ module ValueHistory = struct
     | Call of {f: CallEvent.t; location: Location.t}
     | Capture of {captured_as: Pvar.t; location: Location.t}
     | CppTemporaryCreated of Location.t
-    | VariableDeclaration of Location.t
+    | FormalDeclared of Pvar.t * Location.t
+    | VariableDeclared of Pvar.t * Location.t
   [@@deriving compare]
 
   let pp_event_no_location fmt = function
@@ -136,11 +137,17 @@ module ValueHistory = struct
     | Call {f; location= _} ->
         F.fprintf fmt "returned from call to %a" CallEvent.pp f
     | Capture {captured_as; location= _} ->
-        F.fprintf fmt "value captured as `%a`" (Pvar.pp Pp.text) captured_as
+        F.fprintf fmt "value captured as `%a`" Pvar.pp_value_non_verbose captured_as
     | CppTemporaryCreated _ ->
         F.pp_print_string fmt "C++ temporary created"
-    | VariableDeclaration _ ->
-        F.pp_print_string fmt "variable declared"
+    | FormalDeclared (pvar, _) ->
+        let pp_proc fmt pvar =
+          Pvar.get_declaring_function pvar
+          |> Option.iter ~f:(fun proc_name -> F.fprintf fmt " of %a" Typ.Procname.pp proc_name)
+        in
+        F.fprintf fmt "parameter `%a`%a" Pvar.pp_value_non_verbose pvar pp_proc pvar
+    | VariableDeclared (pvar, _) ->
+        F.fprintf fmt "variable `%a` declared here" Pvar.pp_value_non_verbose pvar
 
 
   let location_of_event = function
@@ -148,7 +155,8 @@ module ValueHistory = struct
     | Call {location}
     | Capture {location}
     | CppTemporaryCreated location
-    | VariableDeclaration location ->
+    | FormalDeclared (_, location)
+    | VariableDeclared (_, location) ->
         location
 
 

infer/src/pulse/PulseDomain.mli

@@ -51,7 +51,8 @@ module ValueHistory : sig
     | Call of {f: CallEvent.t; location: Location.t}
     | Capture of {captured_as: Pvar.t; location: Location.t}
     | CppTemporaryCreated of Location.t
-    | VariableDeclaration of Location.t
+    | FormalDeclared of Pvar.t * Location.t
+    | VariableDeclared of Pvar.t * Location.t
 
   type t = event list [@@deriving compare]
 

infer/src/pulse/PulseOperations.ml

@@ -225,8 +225,10 @@ let eval_deref location exp astate =
   >>| fun astate -> Memory.eval_edge (fst addr_trace) Dereference astate
 
 
-let realloc_var var location astate =
-  Stack.add var (AbstractAddress.mk_fresh (), [ValueHistory.VariableDeclaration location]) astate
+let realloc_pvar pvar location astate =
+  Stack.add (Var.of_pvar pvar)
+    (AbstractAddress.mk_fresh (), [ValueHistory.VariableDeclared (pvar, location)])
+    astate
 
 
 let write_id id new_addr_loc astate = Stack.add (Var.of_id id) new_addr_loc astate

infer/src/pulse/PulseOperations.mli

@@ -57,7 +57,7 @@ val havoc_field :
   -> t
   -> t access_result
 
-val realloc_var : Var.t -> Location.t -> t -> t
+val realloc_pvar : Pvar.t -> Location.t -> t -> t
 
 val write_id : Ident.t -> PulseDomain.Stack.value -> t -> t
 

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -1,10 +1,10 @@
-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,when calling `setLanguage` here,when calling `std::basic_string::~basic_string()` (modelled) here,when calling `deleting the underlying string` (modelled) here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `Range::operator[]` here,invalid access occurs here]
+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,when calling `setLanguage` here,when calling `std::basic_string::~basic_string()` (modelled) here,when calling `deleting the underlying string` (modelled) here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `Range::operator[]` here,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,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,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,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,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 declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here]
-codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here]
-codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,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,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
 codetoanalyze/cpp/pulse/conditionals.cpp, FP_unreachable_ne_then_eq_ok, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int*>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok` here,invalid access occurs here]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_access_ok` here,invalid access occurs here]
@@ -20,11 +20,11 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER
 codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `may_return_invalid_ptr_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,when calling `store` here,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,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap` here,when calling `WrapsB::~WrapsB` here,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `WrapsB::getb`,assigned,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,returned from call to `getwrapperHeap`,invalid access occurs here]
-codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,when calling `getwrapperStack` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,assigned,returned from call to `ReferenceWrapperStack::ReferenceWrapperStack`,returned from call to `getwrapperStack`,invalid access occurs here]
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here]
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here]
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,assigned,returned here]
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,assigned,assigned,returned here]
+codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `b` declared here,when calling `getwrapperStack` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,assigned,returned from call to `ReferenceWrapperStack::ReferenceWrapperStack`,returned from call to `getwrapperStack`,invalid access occurs here]
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,returned here]
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `x` declared here,returned here]
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,assigned,returned here]
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,assigned,assigned,returned here]
 codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `temporaries::UniquePtr<temporaries::A>::~UniquePtr` here,when calling `temporaries::UniquePtr<temporaries::A>::__infer_inner_destructor_~UniquePtr` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `temporaries::UniquePtr<temporaries::A>::get`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
@@ -33,20 +33,20 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DE
 codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `<placement new>()` (modelled),assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `<placement new>()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `use_after_destructor::S::operator=`,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `use_after_destructor::S::S`,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `c` declared here,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `c` declared here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_ok` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok` here,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,when calling `invalidate_local_ok` here,memory is the address of a stack variable `t` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,assigned,returned from call to `invalidate_local_ok`,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `t` declared here,when calling `invalidate_local_ok` here,memory is the address of a stack variable `t` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `t` declared here,assigned,returned from call to `invalidate_local_ok`,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, FP_infeasible_tricky_ok, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, FP_no_free_if_ok, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]