[pulse] do not record addresses of logical variables

Summary:
Before this diff we would record when some values came from the "address
of" logical variables. This makes no sense and also was incorrectly
marking these addresses as "written to" when they appeared in the post
of a procedure, because their attributes weren't empty (they had the
"address of stack variable" attribute).

Reviewed By: ngorogiannis

Differential Revision: D17131210

fbshipit-source-id: 6cc3c465a

infer/src/pulse/PulseAbductiveDomain.ml

@@ -293,7 +293,7 @@ module PrePost = struct
   let filter_for_summary astate =
     let post_stack =
       BaseStack.filter
-        (fun var _ -> not (is_local var astate))
+        (fun var _ -> Var.appears_in_source_code var && not (is_local var astate))
         (astate.post :> PulseDomain.t).stack
     in
     (* deregister empty edges in pre *)

infer/src/pulse/PulseOperations.ml

@@ -303,7 +303,7 @@ let remove_vars vars location astate =
         match Stack.find_opt var astate with
         | Some (address, history) ->
             let astate =
-              if PulseAbductiveDomain.is_local var astate then
+              if Var.appears_in_source_code var && PulseAbductiveDomain.is_local var astate then
                 mark_address_of_stack_variable history var location address astate
               else astate
             in