diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml
index 635226787..9f56d1356 100644
--- a/infer/src/backend/preanal.ml
+++ b/infer/src/backend/preanal.ml
@@ -198,13 +198,15 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
     if Procname.is_java (Procdesc.get_proc_name pdesc)
     then AddressTaken.Domain.empty (* can't take the address of a variable in Java *)
     else
-      match AddressTaken.Analyzer.compute_post (ProcData.make_default pdesc tenv) with
+      let initial = AddressTaken.Domain.empty in
+      match AddressTaken.Analyzer.compute_post (ProcData.make_default pdesc tenv) ~initial with
       | Some post -> post
       | None -> AddressTaken.Domain.empty in
 
   let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc pdesc in
   let nullify_proc_data = ProcData.make pdesc tenv liveness_inv_map in
-  let nullify_inv_map = NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data in
+  let initial = VarDomain.empty, VarDomain.empty in
+  let nullify_inv_map = NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data ~initial in
 
   (* only nullify pvars that are local; don't nullify those that can escape *)
   let is_local pvar =
@@ -258,7 +260,8 @@ module CopyProp =
 
 let do_copy_propagation pdesc tenv =
   let proc_cfg = ExceptionalOneInstrPerNodeCfg.from_pdesc pdesc in
-  let copy_prop_inv_map = CopyProp.exec_cfg proc_cfg (ProcData.make_default pdesc tenv) in
+  let initial = CopyPropagation.Domain.empty in
+  let copy_prop_inv_map = CopyProp.exec_cfg proc_cfg (ProcData.make_default pdesc tenv) ~initial in
   (* [var_map] represents a chain of variable. copies v_0 -> v_1 ... -> v_n. starting from some
      ident v_j, we want to walk backward through the chain to find the lowest v_i that is also an
      ident. *)
@@ -302,8 +305,9 @@ let do_copy_propagation pdesc tenv =
 
 let do_liveness pdesc tenv =
   let liveness_proc_cfg = BackwardCfg.from_pdesc pdesc in
+  let initial = Liveness.Domain.empty in
   let liveness_inv_map =
-    LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default pdesc tenv) in
+    LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default pdesc tenv) ~initial in
   if Config.copy_propagation then do_copy_propagation pdesc tenv;
   add_nullify_instrs pdesc tenv liveness_inv_map;
   Procdesc.signal_did_preanalysis pdesc
diff --git a/infer/src/checkers/AbstractDomain.ml b/infer/src/checkers/AbstractDomain.ml
index dfff8107f..e46f429cc 100644
--- a/infer/src/checkers/AbstractDomain.ml
+++ b/infer/src/checkers/AbstractDomain.ml
@@ -14,19 +14,24 @@ module F = Format
 module type S = sig
   type astate
 
-  val initial : astate
   val (<=) : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *)
   val join : astate -> astate -> astate
   val widen : prev:astate -> next:astate -> num_iters:int -> astate
   val pp : F.formatter -> astate -> unit
 end
 
+module type WithBottom = sig
+  include S
+
+  val empty : astate
+end
+
 module BottomLifted (Domain : S) = struct
   type astate =
     | Bottom
     | NonBottom of Domain.astate
 
-  let initial = Bottom
+  let empty = Bottom
 
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs
@@ -63,8 +68,6 @@ end
 module Pair (Domain1 : S) (Domain2 : S) = struct
   type astate = Domain1.astate * Domain2.astate
 
-  let initial = Domain1.initial, Domain2.initial
-
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs
     then true
@@ -91,8 +94,6 @@ module FiniteSet (S : PrettyPrintable.PPSet) = struct
   include S
   type astate = t
 
-  let initial = empty
-
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs
     then true
@@ -111,8 +112,6 @@ module InvertedSet (S : PrettyPrintable.PPSet) = struct
   include S
   type astate = t
 
-  let initial = empty
-
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs
     then true
@@ -131,8 +130,6 @@ module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
   include M
   type astate = ValueDomain.astate M.t
 
-  let initial = M.empty
-
   (** true if all keys in [lhs] are in [rhs], and each lhs value <= corresponding rhs value *)
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs
@@ -175,8 +172,6 @@ end
 module BooleanAnd = struct
   type astate = bool
 
-  let initial = false
-
   let (<=) ~lhs ~rhs = lhs || not rhs
 
   let join = (&&)
diff --git a/infer/src/checkers/AbstractDomain.mli b/infer/src/checkers/AbstractDomain.mli
index c26f5b754..281368a99 100644
--- a/infer/src/checkers/AbstractDomain.mli
+++ b/infer/src/checkers/AbstractDomain.mli
@@ -16,13 +16,24 @@ module F = Format
 module type S = sig
   type astate
 
-  val initial : astate
-  val (<=) : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *)
+  (** the partial order induced by join *)
+  val (<=) : lhs:astate -> rhs:astate -> bool
+
   val join : astate -> astate -> astate
+
   val widen : prev:astate -> next:astate -> num_iters:int -> astate
+
   val pp : F.formatter -> astate -> unit
 end
 
+(** A domain with an explicit bottom value *)
+module type WithBottom = sig
+  include S
+
+  (** The bottom value of the domain. *)
+  val empty : astate
+end
+
 (** Lift a pre-domain to a domain *)
 module BottomLifted (Domain : S) : sig
   type astate =
@@ -39,7 +50,7 @@ module Pair (Domain1 : S) (Domain2 : S) : S with type astate = Domain1.astate *
     a *finite* collection of possible values, since the widening operator here is just union. *)
 module FiniteSet (Set : PrettyPrintable.PPSet) : sig
   include PrettyPrintable.PPSet with type t = Set.t and type elt = Set.elt
-  include S with type astate = t
+  include WithBottom with type astate = t
 end
 
 (** Lift a set to a powerset domain ordered by superset, so the join operator is intersection *)
@@ -51,7 +62,7 @@ end
 (** Lift a map whose value type is an abstract domain to a domain. *)
 module Map (Map : PrettyPrintable.PPMap) (ValueDomain : S) : sig
   include PrettyPrintable.PPMap with type 'a t = 'a Map.t and type key = Map.key
-  include S with type astate = ValueDomain.astate Map.t
+  include WithBottom with type astate = ValueDomain.astate Map.t
 end
 
 (** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's
diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml
index 900bceba4..0a1dc21a4 100644
--- a/infer/src/checkers/AbstractInterpreter.ml
+++ b/infer/src/checkers/AbstractInterpreter.ml
@@ -20,11 +20,19 @@ module type S = sig
 
   type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
 
-  val compute_post : TransferFunctions.extras ProcData.t -> TransferFunctions.Domain.astate option
+  val compute_post :
+    TransferFunctions.extras ProcData.t ->
+    initial:TransferFunctions.Domain.astate ->
+    TransferFunctions.Domain.astate option
 
-  val exec_cfg : TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> invariant_map
+  val exec_cfg :
+    TransferFunctions.CFG.t ->
+    TransferFunctions.extras ProcData.t ->
+    initial:TransferFunctions.Domain.astate ->
+    invariant_map
 
-  val exec_pdesc : TransferFunctions.extras ProcData.t -> invariant_map
+  val exec_pdesc :
+    TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map
 
   val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option
 
@@ -113,10 +121,10 @@ module MakeNoCFG
         inv_map
 
   (* compute and return an invariant map for [cfg] *)
-  let exec_cfg cfg proc_data =
+  let exec_cfg cfg proc_data ~initial =
     let start_node = CFG.start_node cfg in
     let inv_map', work_queue' =
-      exec_node start_node Domain.initial (Scheduler.empty cfg) InvariantMap.empty proc_data in
+      exec_node start_node initial (Scheduler.empty cfg) InvariantMap.empty proc_data in
     exec_worklist cfg work_queue' inv_map' proc_data
 
   (* compute and return an invariant map for [pdesc] *)
@@ -124,9 +132,9 @@ module MakeNoCFG
     exec_cfg (CFG.from_pdesc pdesc) proc_data
 
   (* compute and return the postcondition of [pdesc] *)
-  let compute_post ({ ProcData.pdesc; } as proc_data) =
+  let compute_post ({ ProcData.pdesc; } as proc_data) ~initial =
     let cfg = CFG.from_pdesc pdesc in
-    let inv_map = exec_cfg cfg proc_data in
+    let inv_map = exec_cfg cfg proc_data ~initial in
     extract_post (CFG.id (CFG.exit_node cfg)) inv_map
 
 end
diff --git a/infer/src/checkers/AbstractInterpreter.mli b/infer/src/checkers/AbstractInterpreter.mli
index 2b49eb8d3..9196529ac 100644
--- a/infer/src/checkers/AbstractInterpreter.mli
+++ b/infer/src/checkers/AbstractInterpreter.mli
@@ -20,14 +20,22 @@ module type S = sig
   (** invariant map from node id -> state representing postcondition for node id *)
   type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
 
-  (** compute and return the postcondition for the given procedure *)
-  val compute_post : TransferFunctions.extras ProcData.t -> TransferFunctions.Domain.astate option
+  (** compute and return the postcondition for the given procedure starting from [initial] *)
+  val compute_post :
+    TransferFunctions.extras ProcData.t ->
+    initial:TransferFunctions.Domain.astate ->
+    TransferFunctions.Domain.astate option
 
-  (** compute and return invariant map for the given CFG/procedure. *)
-  val exec_cfg : TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> invariant_map
+  (** compute and return invariant map for the given CFG/procedure starting from [initial] *)
+  val exec_cfg :
+    TransferFunctions.CFG.t ->
+    TransferFunctions.extras ProcData.t ->
+    initial:TransferFunctions.Domain.astate ->
+    invariant_map
 
-  (** compute and return invariant map for the given procedure. *)
-  val exec_pdesc : TransferFunctions.extras ProcData.t -> invariant_map
+  (** compute and return invariant map for the given procedure starting from [initial] *)
+  val exec_pdesc :
+    TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map
 
   (** extract the postcondition for a node id from the given invariant map *)
   val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option
diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml
index 0aa1250d2..ed3a1d426 100644
--- a/infer/src/checkers/BoundedCallTree.ml
+++ b/infer/src/checkers/BoundedCallTree.ml
@@ -186,5 +186,5 @@ let checker { Callbacks.proc_desc; tenv; get_proc_desc; } =
       SpecSummary.write_summary
         (Procdesc.get_proc_name proc_desc)
         (Some (stacktree_of_pdesc proc_desc "proc_start"));
-      ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv extras))
+      ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv extras) ~initial:Domain.empty)
     end
diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml
index ed959d3eb..8eb00b008 100644
--- a/infer/src/checkers/IdAccessPathMapDomain.ml
+++ b/infer/src/checkers/IdAccessPathMapDomain.ml
@@ -18,8 +18,6 @@ include IdMap
 let pp fmt astate =
   IdMap.pp ~pp_value:AccessPath.pp_raw fmt astate
 
-let initial = IdMap.empty
-
 let (<=) ~lhs ~rhs =
   if phys_equal lhs rhs
   then true
diff --git a/infer/src/checkers/IdAccessPathMapDomain.mli b/infer/src/checkers/IdAccessPathMapDomain.mli
index 2dcdde878..622ba359a 100644
--- a/infer/src/checkers/IdAccessPathMapDomain.mli
+++ b/infer/src/checkers/IdAccessPathMapDomain.mli
@@ -17,4 +17,4 @@ type astate = AccessPath.raw IdMap.t
 
 include (module type of IdMap)
 
-include AbstractDomain.S with type astate := astate
+include AbstractDomain.WithBottom with type astate := astate
diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml
index dfc2819a9..516140402 100644
--- a/infer/src/checkers/SimpleChecker.ml
+++ b/infer/src/checkers/SimpleChecker.ml
@@ -54,8 +54,6 @@ module Make (Spec : Spec) : S = struct
           end)
         )
 
-    let initial = singleton Spec.initial
-
     let widen ~prev ~next ~num_iters =
       let iters_befor_timeout = 1000 in
       (* failsafe for accidental non-finite height domains *)
@@ -103,6 +101,7 @@ module Make (Spec : Spec) : S = struct
           (fun astate ->
              Spec.report astate (ProcCfg.Exceptional.loc node) proc_name)
           astate_set in
-    let inv_map = Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv) in
+    let inv_map =
+      Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv) ~initial:Domain.empty in
     Analyzer.InvariantMap.iter do_reporting inv_map
 end
diff --git a/infer/src/checkers/SinkTrace.ml b/infer/src/checkers/SinkTrace.ml
index 3b85d4a8c..a01b984f6 100644
--- a/infer/src/checkers/SinkTrace.ml
+++ b/infer/src/checkers/SinkTrace.ml
@@ -46,7 +46,7 @@ module Make (TraceElem : TraceElem.S) = struct
 
   type sink_path = Passthroughs.t * (Sink.t * Passthroughs.t) list
 
-  let initial =
+  let empty =
     let dummy_source = () in
     of_source dummy_source
 
@@ -63,7 +63,7 @@ module Make (TraceElem : TraceElem.S) = struct
       (fun t_acc sink ->
          let callee_sink = Sink.with_callsite sink call_site in
          add_sink callee_sink t_acc)
-      initial
+      empty
       (Sinks.elements (sinks t))
 
   let pp fmt t =
diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml
index 4ab565020..9dd34429a 100644
--- a/infer/src/checkers/Siof.ml
+++ b/infer/src/checkers/Siof.ml
@@ -56,7 +56,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       astate
     else
       let trace = match astate with
-        | Domain.Bottom -> SiofTrace.initial
+        | Domain.Bottom -> SiofTrace.empty
         | Domain.NonBottom t -> t in
       let globals_trace =
         SiofTrace.add_sink (SiofTrace.make_access globals outer_loc) trace in
@@ -68,7 +68,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     |> add_globals astate (Procdesc.get_loc pdesc)
 
   let at_least_nonbottom =
-    Domain.join (Domain.NonBottom SiofTrace.initial)
+    Domain.join (Domain.NonBottom SiofTrace.empty)
 
   let exec_instr astate { ProcData.pdesc; } _ (instr : Sil.instr) =
     match instr with
@@ -127,7 +127,7 @@ let report_siof trace pdesc gname loc =
   let trace_of_pname pname =
     match Summary.read_summary pdesc pname with
     | Some (SiofDomain.NonBottom summary) -> summary
-    | _ -> SiofTrace.initial in
+    | _ -> SiofTrace.empty in
 
   let report_one_path (passthroughs, path) =
     let description, sink_path' = match path with
@@ -176,7 +176,7 @@ let siof_check pdesc gname = function
       ()
 
 let compute_post proc_data =
-  Analyzer.compute_post proc_data |> Option.map ~f:SiofDomain.normalize
+  Analyzer.compute_post proc_data ~initial:SiofDomain.Bottom |> Option.map ~f:SiofDomain.normalize
 
 let checker ({ Callbacks.proc_desc; } as callback) =
   let post =
diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml
index cf8510e09..22761e660 100644
--- a/infer/src/checkers/ThreadSafety.ml
+++ b/infer/src/checkers/ThreadSafety.ml
@@ -268,7 +268,7 @@ let make_results_table get_proc_desc file_env =
       (* convert the abstract state to a summary by dropping the id map *)
       let compute_post ({ ProcData.pdesc; tenv; } as proc_data) =
         if not (Procdesc.did_preanalysis pdesc) then Preanal.do_liveness pdesc tenv;
-        match Analyzer.compute_post proc_data with
+        match Analyzer.compute_post proc_data ~initial:ThreadSafetyDomain.empty with
         | Some { locks; reads; writes; } -> Some (locks, reads, writes)
         | None -> None in
       let callback_arg =
@@ -281,9 +281,7 @@ let make_results_table get_proc_desc file_env =
           callback_arg with
       | Some post -> post
       | None ->
-          ThreadSafetyDomain.LocksDomain.initial,
-          ThreadSafetyDomain.PathDomain.initial,
-          ThreadSafetyDomain.PathDomain.initial
+          false, ThreadSafetyDomain.PathDomain.empty, ThreadSafetyDomain.PathDomain.empty
   in
   map_post_computation_over_procs compute_post_for_procedure file_env
 
@@ -314,7 +312,7 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) trace =
   let trace_of_pname callee_pname =
     match Summary.read_summary pdesc callee_pname with
     | Some (_, _, writes) -> writes
-    | _ -> PathDomain.initial in
+    | _ -> PathDomain.empty in
   let report_one_path ((_, sinks) as path) =
     let pp_accesses fmt sink =
       let _, accesses = PathDomain.Sink.kind sink in
diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml
index 259e0af94..44ad763dd 100644
--- a/infer/src/checkers/ThreadSafetyDomain.ml
+++ b/infer/src/checkers/ThreadSafetyDomain.ml
@@ -76,12 +76,12 @@ type astate =
 (** same as astate, but without [id_map] (since it's local) *)
 type summary = LocksDomain.astate * PathDomain.astate * PathDomain.astate
 
-let initial =
-  let locks = LocksDomain.initial in
-  let reads = PathDomain.initial in
-  let writes = PathDomain.initial in
-  let id_map = IdAccessPathMapDomain.initial in
-  let owned = OwnershipDomain.initial in
+let empty =
+  let locks = false in
+  let reads = PathDomain.empty in
+  let writes = PathDomain.empty in
+  let id_map = IdAccessPathMapDomain.empty in
+  let owned = OwnershipDomain.empty in
   { locks; reads; writes; id_map; owned; }
 
 let (<=) ~lhs ~rhs =
diff --git a/infer/src/checkers/Trace.ml b/infer/src/checkers/Trace.ml
index 46edd3141..ba65ed2f4 100644
--- a/infer/src/checkers/Trace.ml
+++ b/infer/src/checkers/Trace.ml
@@ -24,7 +24,7 @@ module type S = sig
   include Spec
   type t
   type astate = t
-  include AbstractDomain.S with type astate := astate
+  include AbstractDomain.WithBottom with type astate := astate
 
   module Sources = Source.Set
   module Sinks = Sink.Set
@@ -35,6 +35,8 @@ module type S = sig
       both the source and sink stack *)
   type path = Passthroughs.t * (Source.t * Passthroughs.t) list * (Sink.t * Passthroughs.t) list
 
+  val empty : t
+
   (** get the sources of the trace. *)
   val sources : t -> Sources.t
 
@@ -377,7 +379,7 @@ module Make (Spec : Spec) = struct
 
       { sources; sinks; passthroughs; }
 
-  let initial =
+  let empty =
     let sources = Sources.empty in
     let sinks = Sinks.empty in
     let passthroughs = Passthroughs.empty in
diff --git a/infer/src/checkers/Trace.mli b/infer/src/checkers/Trace.mli
index 29e388b9f..dd2e3f5ed 100644
--- a/infer/src/checkers/Trace.mli
+++ b/infer/src/checkers/Trace.mli
@@ -24,7 +24,7 @@ module type S = sig
   include Spec
   type t
   type astate = t
-  include AbstractDomain.S with type astate := astate
+  include AbstractDomain.WithBottom with type astate := astate
 
   module Sources = Source.Set
   module Sinks = Sink.Set
@@ -35,6 +35,9 @@ module type S = sig
       both the source and sink stack *)
   type path = Passthroughs.t * (Source.t * Passthroughs.t) list * (Sink.t * Passthroughs.t) list
 
+  (** the empty trace *)
+  val empty : t
+
   (** get the sources of the trace. *)
   val sources : t -> Sources.t
 
diff --git a/infer/src/checkers/accessPathDomains.ml b/infer/src/checkers/accessPathDomains.ml
index acd7854bb..9d9b925b9 100644
--- a/infer/src/checkers/accessPathDomains.ml
+++ b/infer/src/checkers/accessPathDomains.ml
@@ -22,10 +22,10 @@ module Set = struct
       bool recording whether an abstracted access path has been introduced *)
   type astate = APSet.t
 
-  let initial = APSet.empty
-
   let pp = APSet.pp
 
+  let empty = APSet.empty
+
   let normalize aps =
     APSet.filter
       (fun lhs ->
@@ -65,6 +65,6 @@ module Set = struct
         | AccessPath.Exact exact_ap -> APSet.add (AccessPath.Abstracted exact_ap) aps
         | AccessPath.Abstracted _ -> APSet.add ap aps in
       let diff_aps = APSet.diff next prev in
-      APSet.fold abstract_access_path diff_aps initial
+      APSet.fold abstract_access_path diff_aps APSet.empty
       |> join prev
 end
diff --git a/infer/src/checkers/accessPathDomains.mli b/infer/src/checkers/accessPathDomains.mli
index 7a21e2a45..85f5120e0 100644
--- a/infer/src/checkers/accessPathDomains.mli
+++ b/infer/src/checkers/accessPathDomains.mli
@@ -17,7 +17,7 @@ open! IStd
     call to [normalize]. however, [normalize] is quadratic in the size of the set, so it should be
     used sparingly (recommendation: only before computing a summary based on the access path set) *)
 module Set : sig
-  include AbstractDomain.S
+  include AbstractDomain.WithBottom
 
   val of_list : AccessPath.t list -> astate
 
diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml
index 352cb4af6..58f0e5d9a 100644
--- a/infer/src/checkers/accessTree.ml
+++ b/infer/src/checkers/accessTree.ml
@@ -13,7 +13,7 @@ module F = Format
 module L = Logging
 
 module type S = sig
-  module TraceDomain : AbstractDomain.S
+  module TraceDomain : AbstractDomain.WithBottom
   module AccessMap = AccessPath.AccessMap
   module BaseMap = AccessPath.BaseMap
 
@@ -24,9 +24,7 @@ module type S = sig
 
   type t = node BaseMap.t
 
-  include AbstractDomain.S with type astate = t
-
-  val empty : t
+  include AbstractDomain.WithBottom with type astate = t
 
   val empty_node : node
 
@@ -51,7 +49,7 @@ module type S = sig
   val pp_node : F.formatter -> node -> unit
 end
 
-module Make (TraceDomain : AbstractDomain.S) = struct
+module Make (TraceDomain : AbstractDomain.WithBottom) = struct
   module TraceDomain = TraceDomain
   module AccessMap = AccessPath.AccessMap
   module BaseMap = AccessPath.BaseMap
@@ -66,13 +64,11 @@ module Make (TraceDomain : AbstractDomain.S) = struct
 
   let empty = BaseMap.empty
 
-  let initial = empty
-
   let make_node trace subtree =
     trace, Subtree subtree
 
   let empty_node =
-    make_node TraceDomain.initial AccessMap.empty
+    make_node TraceDomain.empty AccessMap.empty
 
   let make_normal_leaf trace =
     make_node trace AccessMap.empty
@@ -217,7 +213,7 @@ module Make (TraceDomain : AbstractDomain.S) = struct
       | access :: accesses, (trace, Subtree subtree) ->
           let access_node =
             try AccessMap.find access subtree
-            with Not_found -> make_normal_leaf TraceDomain.initial in
+            with Not_found -> make_normal_leaf TraceDomain.empty in
           (* once we encounter a subtree rooted in an array access, we have to do weak updates in
              the entire subtree. the reason: if I do x[i].f.g = <interesting trace>, then
              x[j].f.g = <empty trace>, I don't want to overwrite <interesting trace>. instead, I
@@ -234,7 +230,7 @@ module Make (TraceDomain : AbstractDomain.S) = struct
     let is_exact = AccessPath.is_exact ap in
     let base_node =
       try BaseMap.find base tree
-      with Not_found -> make_normal_leaf TraceDomain.initial in
+      with Not_found -> make_normal_leaf TraceDomain.empty in
     let base_node' =
       access_tree_add_trace ~node_to_add ~seen_array_access:false ~is_exact accesses base_node in
     BaseMap.add base base_node' tree
diff --git a/infer/src/checkers/accessTree.mli b/infer/src/checkers/accessTree.mli
index ef201aa3a..b62b05b85 100644
--- a/infer/src/checkers/accessTree.mli
+++ b/infer/src/checkers/accessTree.mli
@@ -9,7 +9,7 @@
 
 (** tree of (trace, access path) associations organized by structure of access paths *)
 module type S = sig
-  module TraceDomain : AbstractDomain.S
+  module TraceDomain : AbstractDomain.WithBottom
   module AccessMap = AccessPath.AccessMap
   module BaseMap = AccessPath.BaseMap
 
@@ -30,9 +30,7 @@ module type S = sig
   *)
   type t = node BaseMap.t
 
-  include AbstractDomain.S with type astate = t
-
-  val empty : t
+  include AbstractDomain.WithBottom with type astate = t
 
   val empty_node : node
 
@@ -69,4 +67,4 @@ module type S = sig
   val pp_node : Format.formatter -> node -> unit
 end
 
-module Make (TraceDomain : AbstractDomain.S) : S with module TraceDomain = TraceDomain
+module Make (TraceDomain : AbstractDomain.WithBottom) : S with module TraceDomain = TraceDomain
diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml
index ea272d5a0..7ae068f19 100644
--- a/infer/src/checkers/annotationReachability.ml
+++ b/infer/src/checkers/annotationReachability.ml
@@ -37,15 +37,6 @@ module Domain = struct
   module TrackingDomain = AbstractDomain.Pair (CallsDomain) (TrackingVar)
   include AbstractDomain.BottomLifted (TrackingDomain)
 
-  let initial =
-    let init_map =
-      IList.fold_left
-        (fun astate_acc (_, snk_annot) -> CallsDomain.add snk_annot CallSiteSet.empty astate_acc)
-        CallsDomain.initial
-        (src_snk_pairs ()) in
-    NonBottom
-      (init_map, TrackingVar.empty)
-
   let add_call key call = function
     | Bottom -> Bottom
     | NonBottom (call_map, vars) as astate ->
@@ -403,8 +394,16 @@ module Interprocedural = struct
       if not (IList.length calls = 0)
       then IList.iter (report_src_snk_path calls) src_annot_list in
 
+    let initial =
+      let init_map =
+        IList.fold_left
+          (fun astate_acc (_, snk_annot) -> CallsDomain.add snk_annot CallSiteSet.empty astate_acc)
+          CallsDomain.empty
+          (src_snk_pairs ()) in
+      Domain.NonBottom
+        (init_map, Domain.TrackingVar.empty) in
     match compute_and_store_post
-            ~compute_post:Analyzer.compute_post
+            ~compute_post:(Analyzer.compute_post ~initial)
             ~make_extras:ProcData.make_empty_extras
             proc_data with
     | Some Domain.NonBottom (call_map, _) ->
diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml
index fd8422341..c79ce2b3c 100644
--- a/infer/src/checkers/copyPropagation.ml
+++ b/infer/src/checkers/copyPropagation.ml
@@ -16,8 +16,6 @@ module Domain = struct
   include Var.Map
   type astate = Var.t Var.Map.t
 
-  let initial = Var.Map.empty
-
   (* return true if the key-value bindings in [rhs] are a subset of the key-value bindings in
      [lhs] *)
   let (<=) ~lhs ~rhs =
diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml
index dc99ec904..7d37f9ac7 100644
--- a/infer/src/checkers/liveness.ml
+++ b/infer/src/checkers/liveness.ml
@@ -59,6 +59,3 @@ module Analyzer =
     (ProcCfg.Backward(ProcCfg.Exceptional))
     (Scheduler.ReversePostorder)
     (TransferFunctions)
-
-let checker { Callbacks.proc_desc; tenv; } =
-  ignore(Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv))
diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
index be20cb3af..8d9a7ccba 100644
--- a/infer/src/quandary/TaintAnalysis.ml
+++ b/infer/src/quandary/TaintAnalysis.ml
@@ -30,7 +30,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
 
       let read_from_payload payload =
         match payload.Specs.quandary with
-        | None -> Some (TaintSpecification.to_summary_access_tree TaintDomain.initial)
+        | None -> Some (TaintSpecification.to_summary_access_tree TaintDomain.empty)
         | summary_opt -> summary_opt
     end)
 
@@ -41,9 +41,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct
         id_map : IdMapDomain.astate; (* mapping of id's to access paths for normalization *)
       }
 
-    let initial =
-      let access_tree = TaintDomain.initial in
-      let id_map = IdMapDomain.initial in
+    let empty =
+      let access_tree = TaintDomain.empty in
+      let id_map = IdMapDomain.empty in
       { access_tree; id_map; }
 
     let (<=) ~lhs ~rhs =
@@ -126,7 +126,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     let access_path_get_trace access_path access_tree proc_data loc =
       match access_path_get_node access_path access_tree proc_data loc with
       | Some (trace, _) -> trace
-      | None -> TraceDomain.initial
+      | None -> TraceDomain.empty
 
     (* get the node associated with [exp] in [access_tree] *)
     let exp_get_node ?(abstracted=false) exp typ { Domain.access_tree; id_map; } proc_data loc =
@@ -172,9 +172,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct
             TaintDomain.fold
               (fun acc _ trace -> TraceDomain.join trace acc)
               (TaintSpecification.of_summary_access_tree summary)
-              TraceDomain.initial
+              TraceDomain.empty
         | None ->
-            TraceDomain.initial in
+            TraceDomain.empty in
 
       let pp_path_short fmt (_, sources_passthroughs, sinks_passthroughs) =
         let original_source = fst (IList.hd sources_passthroughs) in
@@ -394,7 +394,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
               | None -> trace_acc in
             let propagate_to_access_path access_path actuals (astate : Domain.astate) =
               let trace_with_propagation =
-                IList.fold_left exp_join_traces TraceDomain.initial actuals in
+                IList.fold_left exp_join_traces TraceDomain.empty actuals in
               let access_tree =
                 TaintDomain.add_trace access_path trace_with_propagation astate.access_tree in
               { astate with access_tree; } in
@@ -473,7 +473,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                 [called_pname]
               end in
           (* for each possible target of the call, apply the summary. join all results together *)
-          IList.fold_left analyze_call Domain.initial targets
+          IList.fold_left analyze_call Domain.empty targets
       | Sil.Call _ ->
           failwith "Unimp: non-pname call expressions"
       | Sil.Nullify (pvar, _) ->
@@ -507,7 +507,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                base in
            AccessPath.BaseMap.add base' node acc)
         access_tree
-        TaintDomain.initial in
+        TaintDomain.empty in
 
     TaintSpecification.to_summary_access_tree access_tree'
 
@@ -522,7 +522,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
           Preanal.do_liveness proc_data.pdesc proc_data.tenv;
           Preanal.do_dynamic_dispatch proc_data.pdesc (Cg.create None) proc_data.tenv;
         end;
-      match Analyzer.compute_post proc_data with
+      match Analyzer.compute_post proc_data ~initial:Domain.empty with
       | Some { access_tree; } ->
           Some (make_summary proc_data.extras access_tree)
       | None ->
diff --git a/infer/src/unit/BoundedCallTreeTests.ml b/infer/src/unit/BoundedCallTreeTests.ml
index 4aaed0eca..0f3e5aeac 100644
--- a/infer/src/unit/BoundedCallTreeTests.ml
+++ b/infer/src/unit/BoundedCallTreeTests.ml
@@ -21,6 +21,7 @@ let mock_get_proc_desc _ = None
 let tests =
   let open OUnit2 in
   let open AnalyzerTester.StructuredSil in
+  let initial = BoundedCallTree.Domain.empty in
   let f_proc_name = Procname.from_string_c_fun "f" in
   let g_proc_name = Procname.from_string_c_fun "g" in
   let g_args = [((Exp.Const (Const.Cint (IntLit.one))), (Typ.Tint IInt))] in
@@ -66,37 +67,38 @@ let tests =
       make_call ~procname:f_proc_name None [];
       invariant "{ f }"
     ];
-  ] |> TestInterpreter.create_tests ~test_pname:caller_foo_name extras in
+  ] |> TestInterpreter.create_tests
+      ~test_pname:caller_foo_name
+      ~initial:BoundedCallTree.Domain.empty
+      extras in
   let test_list_from_bar = [
     "on_call_anywhere_on_stack_add_proc_name",
     [
       make_call ~procname:f_proc_name None []; (* means f() *)
       invariant "{ f }"
     ];
-  ] |> TestInterpreter.create_tests ~test_pname:caller_bar_name extras in
+  ] |> TestInterpreter.create_tests ~test_pname:caller_bar_name extras ~initial in
   let test_list_from_baz = [
     "ignore_procs_unrelated_to_trace",
     [
       make_call ~procname:f_proc_name None []; (* means f() *)
       invariant "{  }"
     ];
-  ] |> TestInterpreter.create_tests ~test_pname:caller_baz_name extras in
+  ] |> TestInterpreter.create_tests ~test_pname:caller_baz_name extras ~initial in
   let test_list_multiple_traces_from_foo = [
     "on_call_add_proc_name_in_any_stack_1",
     [
       make_call ~procname:f_proc_name None []; (* means f() *)
       invariant "{ f }"
     ];
-  ] |> TestInterpreter.create_tests
-      ~test_pname:caller_foo_name multi_trace_extras in
+  ] |> TestInterpreter.create_tests ~test_pname:caller_foo_name multi_trace_extras ~initial in
   let test_list_multiple_traces_from_bar = [
     "on_call_add_proc_name_in_any_stack_2",
     [
       make_call ~procname:f_proc_name None []; (* means f() *)
       invariant "{ f }"
     ];
-  ] |> TestInterpreter.create_tests
-      ~test_pname:caller_bar_name multi_trace_extras in
+  ] |> TestInterpreter.create_tests ~test_pname:caller_bar_name multi_trace_extras ~initial in
   let test_list = test_list_from_foo @
                   test_list_from_bar @
                   test_list_from_baz @
diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml
index 6bc1013ce..61c37c363 100644
--- a/infer/src/unit/TaintTests.ml
+++ b/infer/src/unit/TaintTests.ml
@@ -255,5 +255,8 @@ let tests =
       invariant "{ ret_id$0 => (SOURCE -> SINK) }";
     ];
 
-  ] |> TestInterpreter.create_tests ~pp_opt:pp_sparse AccessPath.BaseMap.empty in
+  ] |> TestInterpreter.create_tests
+      ~pp_opt:pp_sparse
+      AccessPath.BaseMap.empty
+      ~initial:MockTaintAnalysis.Domain.empty in
   "taint_test_suite">:::test_list
diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml
index c858e48da..a14e0c922 100644
--- a/infer/src/unit/abstractInterpreterTests.ml
+++ b/infer/src/unit/abstractInterpreterTests.ml
@@ -69,6 +69,7 @@ module ExceptionalTestInterpreter = AnalyzerTester.Make
 let tests =
   let open OUnit2 in
   let open AnalyzerTester.StructuredSil in
+  let initial = PathCountDomain.initial in
   let normal_test_list = [
     "straightline",
     [
@@ -180,7 +181,7 @@ let tests =
       );
       invariant "1"
     ];
-  ] |> NormalTestInterpreter.create_tests ProcData.empty_extras in
+  ] |> NormalTestInterpreter.create_tests ProcData.empty_extras ~initial in
   let exceptional_test_list = [
     "try1",
     [
@@ -216,5 +217,5 @@ let tests =
       );
       invariant "3"
     ];
-  ] |> ExceptionalTestInterpreter.create_tests ProcData.empty_extras in
+  ] |> ExceptionalTestInterpreter.create_tests ProcData.empty_extras ~initial in
   "analyzer_tests_suite">:::(normal_test_list @ exceptional_test_list)
diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml
index 8ebcfd672..09dc5db70 100644
--- a/infer/src/unit/accessTreeTests.ml
+++ b/infer/src/unit/accessTreeTests.ml
@@ -14,10 +14,10 @@ module F = Format
 (* string set domain we use to ensure we're getting the expected traces *)
 module MockTraceDomain = struct
   include AbstractDomain.FiniteSet
-    (PrettyPrintable.MakePPSet(struct
-       include String
-       let pp_element fmt s = Format.fprintf fmt "%s" s
-     end))
+      (PrettyPrintable.MakePPSet(struct
+         include String
+         let pp_element fmt s = Format.fprintf fmt "%s" s
+       end))
 
   let top_str = "T"
 
@@ -406,7 +406,7 @@ let tests =
       let x_y_star_base_tree =
         Domain.BaseMap.add
           y_base
-          (Domain.make_starred_leaf MockTraceDomain.initial)
+          (Domain.make_starred_leaf MockTraceDomain.empty)
           x_base_tree in
       assert_trees_equal (widen x_base_tree y_base_tree) x_y_star_base_tree;
 
diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml
index a3e81240a..37bbf6e83 100644
--- a/infer/src/unit/addressTakenTests.ml
+++ b/infer/src/unit/addressTakenTests.ml
@@ -98,5 +98,5 @@ let tests =
       var_assign_addrof_var ~rhs_typ:int_ptr_typ "e" "f";
       invariant "{ &b, &d, &f }"
     ];
-  ] |> TestInterpreter.create_tests ProcData.empty_extras in
+  ] |> TestInterpreter.create_tests ProcData.empty_extras ~initial:AddressTaken.Domain.empty in
   "address_taken_suite">:::test_list
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index aa0816d65..942ba6840 100644
--- a/infer/src/unit/analyzerTester.ml
+++ b/infer/src/unit/analyzerTester.ml
@@ -245,10 +245,10 @@ module Make
     Procdesc.set_exit_node pdesc exit_node;
     pdesc, assert_map
 
-  let create_test test_program extras pp_opt test_pname _ =
+  let create_test test_program extras pp_opt ~initial test_pname _ =
     let pp_state = Option.value ~default:I.TransferFunctions.Domain.pp pp_opt in
     let pdesc, assert_map = structured_program_to_cfg test_program test_pname in
-    let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ()) extras) in
+    let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ()) extras) ~initial in
 
     let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc =
       let post_str =
@@ -279,9 +279,9 @@ module Make
           |> F.flush_str_formatter in
         OUnit2.assert_failure assert_fail_message
 
-  let create_tests ?(test_pname=Procname.empty_block) ?pp_opt extras tests =
+  let create_tests ?(test_pname=Procname.empty_block) ~initial ?pp_opt extras tests =
     let open OUnit2 in
     IList.map (fun (name, test_program) ->
-        name>::create_test test_program extras pp_opt test_pname) tests
+        name>::create_test test_program extras ~initial pp_opt test_pname) tests
 
 end
diff --git a/infer/src/unit/copyPropagationTests.ml b/infer/src/unit/copyPropagationTests.ml
index 9b4074d86..1b3b6e1ce 100644
--- a/infer/src/unit/copyPropagationTests.ml
+++ b/infer/src/unit/copyPropagationTests.ml
@@ -162,5 +162,5 @@ let tests =
       var_assign_id "c" "b";
       invariant "{ &b -> a$0, &c -> b$0 }"
     ];
-  ] |> TestInterpreter.create_tests ProcData.empty_extras in
+  ] |> TestInterpreter.create_tests ProcData.empty_extras ~initial:CopyPropagation.Domain.empty in
   "copy_propagation_test_suite">:::test_list
diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml
index 2bc23ba93..cb7b8db49 100644
--- a/infer/src/unit/livenessTests.ml
+++ b/infer/src/unit/livenessTests.ml
@@ -191,5 +191,5 @@ let tests =
       invariant "{ &b }";
       id_assign_var "a" "b"
     ];
-  ] |> TestInterpreter.create_tests ProcData.empty_extras in
+  ] |> TestInterpreter.create_tests ProcData.empty_extras ~initial:Liveness.Domain.empty in
   "liveness_test_suite">:::test_list