diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt
index cfafd9143..5795200a5 100644
--- a/infer/man/man1/infer-full.txt
+++ b/infer/man/man1/infer-full.txt
@@ -470,6 +470,7 @@ OPTIONS
              PRECONDITION_NOT_FOUND (enabled by default),
              PRECONDITION_NOT_MET (enabled by default),
              PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
+             PULSE_MEMORY_LEAK (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),
              REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by default),
diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt
index fff901c66..63622fe92 100644
--- a/infer/man/man1/infer-report.txt
+++ b/infer/man/man1/infer-report.txt
@@ -201,6 +201,7 @@ OPTIONS
              PRECONDITION_NOT_FOUND (enabled by default),
              PRECONDITION_NOT_MET (enabled by default),
              PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
+             PULSE_MEMORY_LEAK (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),
              REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by default),
diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt
index 52d120802..50e9b761b 100644
--- a/infer/man/man1/infer.txt
+++ b/infer/man/man1/infer.txt
@@ -470,6 +470,7 @@ OPTIONS
              PRECONDITION_NOT_FOUND (enabled by default),
              PRECONDITION_NOT_MET (enabled by default),
              PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
+             PULSE_MEMORY_LEAK (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),
              REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by default),
diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml
index 09cdccba1..50502748b 100644
--- a/infer/src/base/IssueType.ml
+++ b/infer/src/base/IssueType.ml
@@ -406,6 +406,8 @@ let precondition_not_met = register_from_string "PRECONDITION_NOT_MET"
 
 let premature_nil_termination = register_from_string "PREMATURE_NIL_TERMINATION_ARGUMENT"
 
+let pulse_memory_leak = register_from_string ~enabled:false "PULSE_MEMORY_LEAK"
+
 let pure_function = register_from_string "PURE_FUNCTION"
 
 let quandary_taint_error = register_from_string "QUANDARY_TAINT_ERROR"
diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli
index fa07e56e0..286dfb24d 100644
--- a/infer/src/base/IssueType.mli
+++ b/infer/src/base/IssueType.mli
@@ -264,6 +264,8 @@ val precondition_not_met : t
 
 val premature_nil_termination : t
 
+val pulse_memory_leak : t
+
 val pure_function : t
 
 val quandary_taint_error : t
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 81cc9ddcb..4059e2126 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -167,7 +167,8 @@ module PulseTransferFunctions = struct
         dispatch_call tenv summary ret call_exp actuals loc call_flags get_formals astate
         |> check_error summary
     | Metadata (ExitScope (vars, location)) ->
-        [PulseOperations.remove_vars vars location astate]
+        let astate = PulseOperations.remove_vars vars location astate in
+        [check_error summary astate]
     | Metadata (VariableLifetimeBegins (pvar, _, location)) ->
         [PulseOperations.realloc_pvar pvar location astate]
     | Metadata (Abstract _ | Nullify _ | Skip) ->
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 6b910a376..073ffdb56 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -27,6 +27,12 @@ module type BaseDomainSig = sig
   val filter_addr : f:(AbstractValue.t -> bool) -> t -> t
   (**filter both heap and attrs *)
 
+  val partition_addr :
+       f:(AbstractValue.t -> bool)
+    -> t
+    -> (BaseMemory.t * BaseAddressAttributes.t) * (BaseMemory.t * BaseAddressAttributes.t)
+  (**partition both heap and attrs *)
+
   val pp : F.formatter -> t -> unit
 end
 
@@ -54,6 +60,14 @@ module BaseDomainCommon = struct
     let heap' = BaseMemory.filter (fun address _ -> f address) foot.heap in
     let attrs' = BaseAddressAttributes.filter (fun address _ -> f address) foot.attrs in
     update ~heap:heap' ~attrs:attrs' foot
+
+
+  let partition_addr ~f foot =
+    let heap_yes, heap_no = BaseMemory.partition (fun address _ -> f address) foot.heap in
+    let attrs_yes, attrs_no =
+      BaseAddressAttributes.partition (fun address _ -> f address) foot.attrs
+    in
+    ((heap_yes, attrs_yes), (heap_no, attrs_no))
 end
 
 (** represents the post abstract state at each program point *)
@@ -324,11 +338,15 @@ let discard_unreachable ({pre; post} as astate) =
   in
   let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in
   let all_addresses = AbstractValue.Set.union pre_addresses post_addresses in
-  let post_new =
-    Domain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address all_addresses) post
+  let (heap_new, attrs_new), (_, attrs_unreachable) =
+    Domain.partition_addr ~f:(fun address -> AbstractValue.Set.mem address all_addresses) post
+  in
+  let post_new = Domain.update ~heap:heap_new ~attrs:attrs_new post in
+  let astate =
+    if phys_equal pre_new pre && phys_equal post_new post then astate
+    else {astate with pre= pre_new; post= post_new}
   in
-  if phys_equal pre_new pre && phys_equal post_new post then astate
-  else {astate with pre= pre_new; post= post_new}
+  (astate, attrs_unreachable)
 
 
 let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var)
@@ -399,7 +417,9 @@ module PrePost = struct
 
 
   let of_post pdesc astate =
-    filter_for_summary astate |> discard_unreachable |> invalidate_locals pdesc
+    let domain = filter_for_summary astate in
+    let domain, _ = discard_unreachable domain in
+    invalidate_locals pdesc domain
 
 
   (* {2 machinery to apply a pre/post pair corresponding to a function's summary in a function call
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index 1a5b0b666..9300b7f88 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -6,6 +6,7 @@
  *)
 open! IStd
 open PulseBasicInterface
+module BaseAddressAttributes = PulseBaseAddressAttributes
 module BaseDomain = PulseBaseDomain
 module BaseMemory = PulseBaseMemory
 module BaseStack = PulseBaseStack
@@ -103,9 +104,9 @@ end
 
 module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = SkippedTrace.t
 
-val discard_unreachable : t -> t
-(** garbage collect unreachable addresses in the state to make it smaller, just for convenience and
-    keep its size down *)
+val discard_unreachable : t -> t * BaseAddressAttributes.t
+(** [discard_unreachable astate] garbage collects unreachable addresses in the state to make it
+    smaller, and retuns the new state and the attributes of discarded addresses *)
 
 val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t
 
diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml
index 8f50e4aae..41f47c923 100644
--- a/infer/src/pulse/PulseBaseAddressAttributes.ml
+++ b/infer/src/pulse/PulseBaseAddressAttributes.ml
@@ -45,6 +45,8 @@ let empty = Graph.empty
 
 let filter = Graph.filter
 
+let partition = Graph.partition
+
 let pp = Graph.pp
 
 let invalidate (address, history) invalidation location memory =
diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli
index 28ff6ef32..c2e8207c9 100644
--- a/infer/src/pulse/PulseBaseAddressAttributes.mli
+++ b/infer/src/pulse/PulseBaseAddressAttributes.mli
@@ -14,6 +14,8 @@ val empty : t
 
 val filter : (AbstractValue.t -> Attributes.t -> bool) -> t -> t
 
+val partition : (AbstractValue.t -> Attributes.t -> bool) -> t -> t * t
+
 val find_opt : AbstractValue.t -> t -> Attributes.t option
 
 val add_one : AbstractValue.t -> Attribute.t -> t -> t
diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml
index 724f827bc..307ead84a 100644
--- a/infer/src/pulse/PulseDiagnostic.ml
+++ b/infer/src/pulse/PulseDiagnostic.ml
@@ -15,12 +15,13 @@ module ValueHistory = PulseValueHistory
 type t =
   | AccessToInvalidAddress of
       {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t}
+  | MemoryLeak of {allocation_trace: Trace.t; location: Location.t}
   | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
 
 let get_location = function
   | AccessToInvalidAddress {access_trace} ->
       Trace.get_outer_location access_trace
-  | StackVariableAddressEscape {location} ->
+  | MemoryLeak {location} | StackVariableAddressEscape {location} ->
       location
 
 
@@ -66,6 +67,20 @@ let get_message = function
       F.asprintf "%a%a" pp_access_trace access_trace
         (pp_invalidation_trace invalidation_line invalidation)
         invalidation_trace
+  | MemoryLeak {location; allocation_trace} ->
+      let allocation_line =
+        let {Location.line; _} = Trace.get_outer_location allocation_trace in
+        line
+      in
+      let pp_allocation_trace fmt (trace : Trace.t) =
+        match trace with
+        | Immediate _ ->
+            F.fprintf fmt "by call to `malloc()`"
+        | ViaCall {f; _} ->
+            F.fprintf fmt "by call to %a" CallEvent.describe f
+      in
+      F.asprintf "memory dynamically allocated at line %d %a, is not reachable after %a"
+        allocation_line pp_allocation_trace allocation_trace Location.pp location
   | StackVariableAddressEscape {variable; _} ->
       let pp_var f var =
         if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary"
@@ -95,6 +110,13 @@ let get_trace = function
            ~pp_immediate:(fun fmt -> F.pp_print_string fmt "invalid access occurs here")
            access_trace
       @@ []
+  | MemoryLeak {allocation_trace} ->
+      let access_start_location = Trace.get_start_location allocation_trace in
+      add_errlog_header ~title:"allocation part of the trace starts here" access_start_location
+      @@ Trace.add_to_errlog ~nesting:0
+           ~pp_immediate:(fun fmt -> F.pp_print_string fmt "allocation occurs here")
+           allocation_trace
+      @@ []
   | StackVariableAddressEscape {history; location; _} ->
       ValueHistory.add_to_errlog ~nesting:0 history
       @@
@@ -105,5 +127,7 @@ let get_trace = function
 let get_issue_type = function
   | AccessToInvalidAddress {invalidation; _} ->
       Invalidation.issue_type_of_cause invalidation
+  | MemoryLeak _ ->
+      IssueType.pulse_memory_leak
   | StackVariableAddressEscape _ ->
       IssueType.stack_variable_address_escape
diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli
index 3b94721d3..f07ffb7a5 100644
--- a/infer/src/pulse/PulseDiagnostic.mli
+++ b/infer/src/pulse/PulseDiagnostic.mli
@@ -14,6 +14,7 @@ module ValueHistory = PulseValueHistory
 type t =
   | AccessToInvalidAddress of
       {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t}
+  | MemoryLeak of {allocation_trace: Trace.t; location: Location.t}
   | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
 
 val get_message : t -> string
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index 2c043eeef..d9bcdff89 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -468,6 +468,29 @@ 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 _ attributes result =
+    let allocated_not_freed_opt =
+      Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *))
+        ~f:(fun acc attr ->
+          match (attr : Attribute.t) with
+          | Allocated trace ->
+              (Some trace, snd acc)
+          | Invalid (CFree, _) ->
+              (fst acc, true)
+          | _ ->
+              acc )
+    in
+    match allocated_not_freed_opt with
+    | Some trace, false ->
+        (* allocated but not freed *)
+        Error (Diagnostic.MemoryLeak {location; allocation_trace= trace})
+    | _ ->
+        result
+  in
+  PulseBaseAddressAttributes.fold check_memory_leak unreachable_attrs (Ok ())
+
+
 let remove_vars vars location astate =
   let astate =
     List.fold vars ~init:astate ~f:(fun astate var ->
@@ -485,7 +508,11 @@ let remove_vars vars location astate =
             astate )
   in
   let astate' = Stack.remove_vars vars astate in
-  if phys_equal astate' astate then astate else AbductiveDomain.discard_unreachable 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
+    astate
 
 
 let is_ptr_to_const formal_typ_opt =
diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli
index 2b9603265..b36e1e5d1 100644
--- a/infer/src/pulse/PulseOperations.mli
+++ b/infer/src/pulse/PulseOperations.mli
@@ -99,7 +99,7 @@ val shallow_copy :
   -> (t * (AbstractValue.t * ValueHistory.t)) access_result
 (** returns the address of a new cell with the same edges as the original *)
 
-val remove_vars : Var.t list -> Location.t -> t -> t
+val remove_vars : Var.t list -> Location.t -> t -> t access_result
 
 val check_address_escape :
   Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result
diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp
index e69de29bb..92634d016 100644
--- a/infer/tests/codetoanalyze/c/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/c/pulse/issues.exp
@@ -0,0 +1,3 @@
+codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocation occurs here]
+codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here]
+codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here]
diff --git a/infer/tests/codetoanalyze/c/pulse/memory_leak.c b/infer/tests/codetoanalyze/c/pulse/memory_leak.c
index a93b6b0d6..5b430a8bf 100644
--- a/infer/tests/codetoanalyze/c/pulse/memory_leak.c
+++ b/infer/tests/codetoanalyze/c/pulse/memory_leak.c
@@ -6,9 +6,7 @@
  */
 #include <stdlib.h>
 
-void malloc_no_free_bad() { // TODO implement the check
-  int* p = malloc(sizeof(p));
-}
+void malloc_no_free_bad() { int* p = malloc(sizeof(p)); }
 
 int* malloc_returned_ok() {
   int* p = malloc(sizeof(p));
@@ -20,3 +18,17 @@ void malloc_then_free_ok() {
   *p = 5;
   free(p);
 }
+
+int* create_p() {
+  int* p = malloc(sizeof(p));
+  return p;
+}
+
+void malloc_interproc_no_free_bad() { int* p = create_p(); }
+
+void malloc_interproc_no_free_bad2() {
+  int* p = malloc(sizeof(p));
+  int z = 3;
+  int y = 4;
+  int* q = p;
+}