diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index a56742eb4..ba298251f 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -31,6 +31,9 @@ module ItvPure : sig
 
   val nat : t
 
+  val pos : t
+  (** [1, +oo] *)
+
   val of_int : int -> t
 
   val lb : t -> Bound.t
diff --git a/infer/src/pulse/PulseCItv.ml b/infer/src/pulse/PulseCItv.ml
index d43568fba..fbd3dbb50 100644
--- a/infer/src/pulse/PulseCItv.ml
+++ b/infer/src/pulse/PulseCItv.ml
@@ -121,6 +121,8 @@ module Unsafe : sig
   val equal_to : IntLit.t -> t
 
   val not_equal_to : IntLit.t -> t
+
+  val ge_to : IntLit.t -> t
 end = struct
   type t = Between of Bound.t * Bound.t | Outside of IntLit.t * IntLit.t [@@deriving compare]
 
@@ -140,6 +142,10 @@ end = struct
 
 
   let not_equal_to i = Outside (i, i)
+
+  let ge_to i =
+    let b = Bound.Int i in
+    Between (b, Bound.PlusInfinity)
 end
 
 include Unsafe
diff --git a/infer/src/pulse/PulseCItv.mli b/infer/src/pulse/PulseCItv.mli
index 92fbbd863..a70ecd2d9 100644
--- a/infer/src/pulse/PulseCItv.mli
+++ b/infer/src/pulse/PulseCItv.mli
@@ -39,3 +39,5 @@ val binop : Binop.t -> t -> t -> t option
 val unop : Unop.t -> t -> t option
 
 val zero_inf : t
+
+val ge_to : IntLit.t -> t
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 2019fa076..a0a053022 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -88,10 +88,25 @@ module C = struct
       [astate]
 
 
-  let malloc access : model =
+  let malloc _ : model =
    fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate ->
-    let astate = PulseOperations.allocate callee_procname location access astate in
-    Ok [PulseOperations.write_id ret_id access astate]
+    let ret_addr = AbstractValue.mk_fresh () in
+    let astate_alloc =
+      PulseOperations.allocate callee_procname location (ret_addr, []) astate
+      |> PulseOperations.write_id ret_id (ret_addr, [])
+      |> AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.pos)
+      |> AddressAttributes.add_one ret_addr
+           (CItv (CItv.ge_to IntLit.one, Immediate {location; history= []}))
+    in
+    let+ astate_null =
+      AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit IntLit.zero)) astate
+      |> AddressAttributes.add_one ret_addr
+           (CItv (CItv.equal_to IntLit.zero, Immediate {location; history= []}))
+      |> PulseOperations.write_id ret_id (ret_addr, [])
+      |> PulseOperations.invalidate location (Invalidation.ConstantDereference IntLit.zero)
+           (ret_addr, [])
+    in
+    [astate_alloc; astate_null]
 end
 
 module Cplusplus = struct
diff --git a/infer/tests/codetoanalyze/c/pulse/memory_leak.c b/infer/tests/codetoanalyze/c/pulse/memory_leak.c
index 5b430a8bf..a568be0d1 100644
--- a/infer/tests/codetoanalyze/c/pulse/memory_leak.c
+++ b/infer/tests/codetoanalyze/c/pulse/memory_leak.c
@@ -15,8 +15,10 @@ int* malloc_returned_ok() {
 
 void malloc_then_free_ok() {
   int* p = malloc(sizeof(p));
-  *p = 5;
-  free(p);
+  if (p) {
+    *p = 5;
+    free(p);
+  }
 }
 
 int* create_p() {