diff --git a/Makefile b/Makefile
index dbf28927e..ee74af76d 100644
--- a/Makefile
+++ b/Makefile
@@ -55,6 +55,7 @@ DIRECT_TESTS += \
   c_errors \
   c_frontend \
   c_performance \
+  c_pulse \
   c_purity \
   c_uninit \
   cpp_annotation-reachability \
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 77b7a678f..d3446d458 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -203,6 +203,10 @@ module AddressAttributes = struct
     map_post_attrs astate ~f:(BaseAddressAttributes.invalidate address invalidation location)
 
 
+  let allocate address location astate =
+    map_post_attrs astate ~f:(BaseAddressAttributes.allocate address location)
+
+
   let add_one address attributes astate =
     map_post_attrs astate ~f:(BaseAddressAttributes.add_one address attributes)
 
@@ -662,6 +666,7 @@ module PrePost = struct
       )
     | AddressOfCppTemporary _
     | AddressOfStackVariable _
+    | Allocated _
     | Closure _
     | Invalid _
     | MustBeValid _
@@ -681,6 +686,8 @@ module PrePost = struct
       | Arithmetic (arith, trace) ->
           Attribute.Arithmetic
             (arith, add_call_to_trace proc_name call_location caller_history trace)
+      | Allocated trace ->
+          Attribute.Allocated (add_call_to_trace proc_name call_location caller_history trace)
       | AddressOfCppTemporary _
       | AddressOfStackVariable _
       | BoItv _
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index 0ec3674b3..0f985d8f5 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -76,6 +76,8 @@ module AddressAttributes : sig
 
   val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
+  val allocate : AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
+
   val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
   val is_std_vector_reserved : AbstractValue.t -> t -> bool
diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml
index 5fb510ec1..adf8415de 100644
--- a/infer/src/pulse/PulseAttribute.ml
+++ b/infer/src/pulse/PulseAttribute.ml
@@ -28,6 +28,7 @@ module Attribute = struct
   type t =
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
+    | Allocated of Trace.t
     | Arithmetic of Arithmetic.t * Trace.t
     | BoItv of Itv.ItvPure.t
     | Closure of Procname.t
@@ -75,6 +76,8 @@ module Attribute = struct
         F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history
     | AddressOfStackVariable (var, location, history) ->
         F.fprintf f "s&%a (%a) at %a" Var.pp var ValueHistory.pp history Location.pp location
+    | Allocated trace ->
+        F.fprintf f "Allocated %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "allocation")) trace
     | BoItv bo_itv ->
         F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv
     | Closure pname ->
@@ -164,6 +167,7 @@ let is_suitable_for_pre = function
       true
   | AddressOfCppTemporary _
   | AddressOfStackVariable _
+  | Allocated _
   | Closure _
   | Invalid _
   | StdVectorReserve
diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli
index dd8c8d6f8..6a56ad007 100644
--- a/infer/src/pulse/PulseAttribute.mli
+++ b/infer/src/pulse/PulseAttribute.mli
@@ -14,6 +14,7 @@ module ValueHistory = PulseValueHistory
 type t =
   | AddressOfCppTemporary of Var.t * ValueHistory.t
   | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
+  | Allocated of Trace.t
   | Arithmetic of Arithmetic.t * Trace.t
   | BoItv of Itv.ItvPure.t
   | Closure of Procname.t
diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml
index d0c0f8538..67fb3b83e 100644
--- a/infer/src/pulse/PulseBaseAddressAttributes.ml
+++ b/infer/src/pulse/PulseBaseAddressAttributes.ml
@@ -51,6 +51,10 @@ let invalidate (address, history) invalidation location memory =
   add_one address (Attribute.Invalid (invalidation, Immediate {location; history})) memory
 
 
+let allocate (address, history) location memory =
+  add_one address (Attribute.Allocated (Immediate {location; history})) memory
+
+
 let check_valid address attrs =
   L.d_printfln "Checking validity of %a" AbstractValue.pp address ;
   match Graph.find_opt address attrs |> Option.bind ~f:Attributes.get_invalid with
diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli
index 140e4fd6a..a510ac6ed 100644
--- a/infer/src/pulse/PulseBaseAddressAttributes.mli
+++ b/infer/src/pulse/PulseBaseAddressAttributes.mli
@@ -20,6 +20,8 @@ val add_one : AbstractValue.t -> Attribute.t -> t -> t
 
 val add : AbstractValue.t -> Attributes.t -> t -> t
 
+val allocate : AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
+
 val fold : (AbstractValue.t -> Attributes.t -> 'a -> 'a) -> t -> 'a -> 'a
 
 val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) result
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 654761212..7e904bc50 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -87,6 +87,12 @@ module C = struct
     else
       let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in
       [astate]
+
+
+  let malloc access : model =
+   fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
+    let astate = PulseOperations.allocate location access astate in
+    Ok [PulseOperations.write_id ret_id access astate]
 end
 
 module Cplusplus = struct
@@ -397,6 +403,7 @@ module ProcNameDispatcher = struct
     let pushback_modeled = StringSet.of_list ["add"; "put"; "addAll"; "putAll"; "remove"] in
     make_dispatcher
       [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
+      ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc
       ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete
       ; +match_builtin BuiltinDecl.__placement_new &++> Cplusplus.placement_new
       ; +match_builtin BuiltinDecl.objc_cpp_throw <>--> Misc.early_exit
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index 86baa234e..5bfeace1f 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -376,6 +376,8 @@ let havoc_field location addr_trace field trace_obj astate =
   write_field location addr_trace field (AbstractValue.mk_fresh (), trace_obj) astate
 
 
+let allocate location addr_trace astate = AddressAttributes.allocate addr_trace location astate
+
 let invalidate location cause addr_trace astate =
   check_addr_access location addr_trace astate
   >>| AddressAttributes.invalidate addr_trace cause location
diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli
index f2e827a48..2b9603265 100644
--- a/infer/src/pulse/PulseOperations.mli
+++ b/infer/src/pulse/PulseOperations.mli
@@ -82,6 +82,8 @@ val invalidate :
   Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
 (** record that the address is invalid *)
 
+val allocate : Location.t -> AbstractValue.t * ValueHistory.t -> t -> t
+
 val invalidate_deref :
   Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
 (** record that what the address points to is invalid *)
diff --git a/infer/tests/codetoanalyze/c/pulse/Makefile b/infer/tests/codetoanalyze/c/pulse/Makefile
new file mode 100644
index 000000000..4b936314b
--- /dev/null
+++ b/infer/tests/codetoanalyze/c/pulse/Makefile
@@ -0,0 +1,15 @@
+# Copyright (c) Facebook, Inc. and its affiliates.
+#
+# This source code is licensed under the MIT license found in the
+# LICENSE file in the root directory of this source tree.
+
+TESTS_DIR = ../../..
+
+CLANG_OPTIONS = -c
+INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR)
+
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.c)
+
+include $(TESTS_DIR)/clang.make
diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp
new file mode 100644
index 000000000..e69de29bb
diff --git a/infer/tests/codetoanalyze/c/pulse/memory_leak.c b/infer/tests/codetoanalyze/c/pulse/memory_leak.c
new file mode 100644
index 000000000..a93b6b0d6
--- /dev/null
+++ b/infer/tests/codetoanalyze/c/pulse/memory_leak.c
@@ -0,0 +1,22 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stdlib.h>
+
+void malloc_no_free_bad() { // TODO implement the check
+  int* p = malloc(sizeof(p));
+}
+
+int* malloc_returned_ok() {
+  int* p = malloc(sizeof(p));
+  return p;
+}
+
+void malloc_then_free_ok() {
+  int* p = malloc(sizeof(p));
+  *p = 5;
+  free(p);
+}