From 9487cab1452efbac5ee5b22d0d7fffd20521e27b Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 13 Jul 2016 15:56:31 -0700
Subject: [PATCH] Refactor Sil.const into separate Const module

Summary: Move Sil.const type and operations into separate Const module.

Reviewed By: dulmarod

Differential Revision: D3548073

fbshipit-source-id: 388d03e
---
 infer/src/IR/Cfg.re                          |  16 +-
 infer/src/IR/Const.re                        |  84 +++++++
 infer/src/IR/Const.rei                       |  45 ++++
 infer/src/IR/Sil.re                          |  74 +-----
 infer/src/IR/Sil.rei                         |  27 +--
 infer/src/backend/abs.ml                     |  10 +-
 infer/src/backend/absarray.ml                |   2 +-
 infer/src/backend/autounit.ml                |  30 +--
 infer/src/backend/buckets.ml                 |   4 +-
 infer/src/backend/dom.ml                     |  30 +--
 infer/src/backend/dotty.ml                   |   2 +-
 infer/src/backend/errdesc.ml                 |  16 +-
 infer/src/backend/match.ml                   |   2 +-
 infer/src/backend/modelBuiltins.ml           |  26 +--
 infer/src/backend/preanal.ml                 |   2 +-
 infer/src/backend/prop.ml                    | 231 ++++++++++---------
 infer/src/backend/prover.ml                  | 127 +++++-----
 infer/src/backend/rearrange.ml               |   8 +-
 infer/src/backend/state.ml                   |   2 +-
 infer/src/backend/state.mli                  |   2 +-
 infer/src/backend/symExec.ml                 |  46 ++--
 infer/src/backend/tabulation.ml              |   6 +-
 infer/src/checkers/checkTraceCallSequence.ml |   8 +-
 infer/src/checkers/checkers.ml               |  17 +-
 infer/src/checkers/codeQuery.ml              |   4 +-
 infer/src/checkers/constantPropagation.ml    |  25 +-
 infer/src/checkers/constantPropagation.mli   |   2 +-
 infer/src/checkers/dataflow.ml               |   4 +-
 infer/src/checkers/patternMatch.ml           |  14 +-
 infer/src/checkers/patternMatch.mli          |   2 +-
 infer/src/checkers/printfArgs.ml             |   4 +-
 infer/src/checkers/repeatedCallsChecker.ml   |   6 +-
 infer/src/checkers/sqlChecker.ml             |   4 +-
 infer/src/clang/cArithmetic_trans.ml         |  16 +-
 infer/src/clang/cTrans.ml                    |  52 ++---
 infer/src/clang/cTrans_models.ml             |  15 +-
 infer/src/clang/cTrans_utils.ml              |  16 +-
 infer/src/eradicate/eradicateChecks.ml       |   2 +-
 infer/src/eradicate/typeCheck.ml             |  42 ++--
 infer/src/harness/inhabit.ml                 |   8 +-
 infer/src/java/jTrans.ml                     |  42 ++--
 infer/src/java/jTransExn.ml                  |   4 +-
 infer/src/java/jTransStaticField.ml          |   4 +-
 infer/src/llvm/lTrans.ml                     |   4 +-
 infer/src/unit/analyzerTester.ml             |   2 +-
 45 files changed, 571 insertions(+), 518 deletions(-)
 create mode 100644 infer/src/IR/Const.re
 create mode 100644 infer/src/IR/Const.rei

diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re
index b8ee2202b..4715aad06 100644
--- a/infer/src/IR/Cfg.re
+++ b/infer/src/IR/Cfg.re
@@ -347,7 +347,7 @@ let module Node = {
       switch instr {
       | Sil.Call _ exp _ _ _ =>
         switch exp {
-        | Sil.Const (Sil.Cfun procname) => [procname, ...callees]
+        | Sil.Const (Const.Cfun procname) => [procname, ...callees]
         | _ => callees
         }
       | _ => callees
@@ -700,7 +700,7 @@ let module Node = {
         }
       | Sil.Call
           return_ids
-          (Sil.Const (Sil.Cfun (Procname.Java callee_pname_java)))
+          (Sil.Const (Const.Cfun (Procname.Java callee_pname_java)))
           [(Sil.Var id, _), ...origin_args]
           loc
           call_flags
@@ -714,7 +714,7 @@ let module Node = {
             [(Sil.Var id, redirected_typ), ...other_args]
           };
           let call_instr =
-            Sil.Call return_ids (Sil.Const (Sil.Cfun redirected_pname)) args loc call_flags;
+            Sil.Call return_ids (Sil.Const (Const.Cfun redirected_pname)) args loc call_flags;
           [call_instr, ...instrs]
         }
       | Sil.Call return_ids origin_call_exp origin_args loc call_flags => {
@@ -1198,11 +1198,11 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr =>
       /* setter for static fields */
       let instr' = Sil.Set (Sil.Lfield (Sil.Lvar pvar) fn ft) bt e1 loc_call;
       found instr instr'
-    | (Sil.Call ret_ids' (Sil.Const (Sil.Cfun pn)) etl' _ cf, _, _)
+    | (Sil.Call ret_ids' (Sil.Const (Const.Cfun pn)) etl' _ cf, _, _)
         when IList.length ret_ids == IList.length ret_ids' && IList.length etl' == IList.length etl =>
-      let instr' = Sil.Call ret_ids (Sil.Const (Sil.Cfun pn)) etl loc_call cf;
+      let instr' = Sil.Call ret_ids (Sil.Const (Const.Cfun pn)) etl loc_call cf;
       found instr instr'
-    | (Sil.Call ret_ids' (Sil.Const (Sil.Cfun pn)) etl' _ cf, _, _)
+    | (Sil.Call ret_ids' (Sil.Const (Const.Cfun pn)) etl' _ cf, _, _)
         when
           IList.length ret_ids == IList.length ret_ids' &&
             IList.length etl' + 1 == IList.length etl =>
@@ -1212,7 +1212,7 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr =>
         | [_, ...l] => IList.rev l
         | [] => assert false
         };
-      let instr' = Sil.Call ret_ids (Sil.Const (Sil.Cfun pn)) etl1 loc_call cf;
+      let instr' = Sil.Call ret_ids (Sil.Const (Const.Cfun pn)) etl1 loc_call cf;
       found instr instr'
     | _ => ()
     };
@@ -1225,7 +1225,7 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr =>
 let proc_inline_synthetic_methods cfg proc_desc :unit => {
   let instr_inline_synthetic_method =
     fun
-    | Sil.Call ret_ids (Sil.Const (Sil.Cfun pn)) etl loc _ =>
+    | Sil.Call ret_ids (Sil.Const (Const.Cfun pn)) etl loc _ =>
       switch (Procdesc.find_from_name cfg pn) {
       | Some pd =>
         let is_access = Procname.java_is_access_method pn;
diff --git a/infer/src/IR/Const.re b/infer/src/IR/Const.re
new file mode 100644
index 000000000..3c525dea5
--- /dev/null
+++ b/infer/src/IR/Const.re
@@ -0,0 +1,84 @@
+/*
+ * vim: set ft=rust:
+ * vim: set ft=reason:
+ *
+ * Copyright (c) 2009 - 2013 Monoidics ltd.
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+open! Utils;
+
+
+/** The Smallfoot Intermediate Language: Constants */
+let module L = Logging;
+
+let module F = Format;
+
+type t =
+  | Cint of IntLit.t /** integer constants */
+  | Cfun of Procname.t /** function names */
+  | Cstr of string /** string constants */
+  | Cfloat of float /** float constants */
+  | Cclass of Ident.name /** class constant */
+  | Cptr_to_fld of Ident.fieldname Typ.t /** pointer to field constant,
+                                             and type of the surrounding Csu.t type */;
+
+let compare (c1: t) (c2: t) :int =>
+  switch (c1, c2) {
+  | (Cint i1, Cint i2) => IntLit.compare i1 i2
+  | (Cint _, _) => (-1)
+  | (_, Cint _) => 1
+  | (Cfun fn1, Cfun fn2) => Procname.compare fn1 fn2
+  | (Cfun _, _) => (-1)
+  | (_, Cfun _) => 1
+  | (Cstr s1, Cstr s2) => string_compare s1 s2
+  | (Cstr _, _) => (-1)
+  | (_, Cstr _) => 1
+  | (Cfloat f1, Cfloat f2) => float_compare f1 f2
+  | (Cfloat _, _) => (-1)
+  | (_, Cfloat _) => 1
+  | (Cclass c1, Cclass c2) => Ident.name_compare c1 c2
+  | (Cclass _, _) => (-1)
+  | (_, Cclass _) => 1
+  | (Cptr_to_fld fn1 t1, Cptr_to_fld fn2 t2) =>
+    let n = Ident.fieldname_compare fn1 fn2;
+    if (n != 0) {
+      n
+    } else {
+      Typ.compare t1 t2
+    }
+  };
+
+let equal c1 c2 => compare c1 c2 == 0;
+
+let kind_equal c1 c2 => {
+  let const_kind_number =
+    fun
+    | Cint _ => 1
+    | Cfun _ => 2
+    | Cstr _ => 3
+    | Cfloat _ => 4
+    | Cclass _ => 5
+    | Cptr_to_fld _ => 6;
+  const_kind_number c1 == const_kind_number c2
+};
+
+let pp pe f =>
+  fun
+  | Cint i => IntLit.pp f i
+  | Cfun fn =>
+    switch pe.pe_kind {
+    | PP_HTML => F.fprintf f "_fun_%s" (Escape.escape_xml (Procname.to_string fn))
+    | _ => F.fprintf f "_fun_%s" (Procname.to_string fn)
+    }
+  | Cstr s => F.fprintf f "\"%s\"" (String.escaped s)
+  | Cfloat v => F.fprintf f "%f" v
+  | Cclass c => F.fprintf f "%a" Ident.pp_name c
+  | Cptr_to_fld fn _ => F.fprintf f "__fld_%a" Ident.pp_fieldname fn;
+
+let to_string c => pp_to_string (pp pe_text) c;
diff --git a/infer/src/IR/Const.rei b/infer/src/IR/Const.rei
new file mode 100644
index 000000000..90d352b07
--- /dev/null
+++ b/infer/src/IR/Const.rei
@@ -0,0 +1,45 @@
+/*
+ * vim: set ft=rust:
+ * vim: set ft=reason:
+ *
+ * Copyright (c) 2009 - 2013 Monoidics ltd.
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+open! Utils;
+
+
+/** The Smallfoot Intermediate Language: Constants */
+let module L = Logging;
+
+let module F = Format;
+
+
+/** Constants */
+type t =
+  | Cint of IntLit.t /** integer constants */
+  | Cfun of Procname.t /** function names */
+  | Cstr of string /** string constants */
+  | Cfloat of float /** float constants */
+  | Cclass of Ident.name /** class constant */
+  | Cptr_to_fld of Ident.fieldname Typ.t /** pointer to field constant,
+                                             and type of the surrounding Csu.t type */;
+
+let compare: t => t => int;
+
+let equal: t => t => bool;
+
+
+/** Return true if the constants have the same kind (both integers, ...) */
+let kind_equal: t => t => bool;
+
+
+/** Pretty print a const */
+let pp: printenv => F.formatter => t => unit;
+
+let to_string: t => string;
diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re
index d01eef4de..3c8cd29e9 100644
--- a/infer/src/IR/Sil.re
+++ b/infer/src/IR/Sil.re
@@ -415,22 +415,11 @@ type taint_kind =
 type taint_info = {taint_source: Procname.t, taint_kind: taint_kind};
 
 
-/** Constants */
-type const =
-  | Cint of IntLit.t /** integer constants */
-  | Cfun of Procname.t /** function names */
-  | Cstr of string /** string constants */
-  | Cfloat of float /** float constants */
-  | Cclass of Ident.name /** class constant */
-  | Cptr_to_fld of Ident.fieldname Typ.t /** pointer to field constant,
-                                             and type of the surrounding Csu.t type */;
-
-
 /** expression representing the result of decompilation */
 type dexp =
   | Darray of dexp dexp
   | Dbinop of binop dexp dexp
-  | Dconst of const
+  | Dconst of Const.t
   | Dsizeof of Typ.t (option dexp) Subtype.t
   | Dderef of dexp
   | Dfcall of dexp (list dexp) Location.t call_flags
@@ -496,7 +485,7 @@ and exp =
   /** Anonymous function */
   | Closure of closure
   /** Constants */
-  | Const of const
+  | Const of Const.t
   /** Type cast */
   | Cast of Typ.t exp
   /** The address of a program variable */
@@ -987,46 +976,6 @@ let attr_is_undef =
   | Aundef _ => true
   | _ => false;
 
-let const_compare (c1: const) (c2: const) :int =>
-  switch (c1, c2) {
-  | (Cint i1, Cint i2) => IntLit.compare i1 i2
-  | (Cint _, _) => (-1)
-  | (_, Cint _) => 1
-  | (Cfun fn1, Cfun fn2) => Procname.compare fn1 fn2
-  | (Cfun _, _) => (-1)
-  | (_, Cfun _) => 1
-  | (Cstr s1, Cstr s2) => string_compare s1 s2
-  | (Cstr _, _) => (-1)
-  | (_, Cstr _) => 1
-  | (Cfloat f1, Cfloat f2) => float_compare f1 f2
-  | (Cfloat _, _) => (-1)
-  | (_, Cfloat _) => 1
-  | (Cclass c1, Cclass c2) => Ident.name_compare c1 c2
-  | (Cclass _, _) => (-1)
-  | (_, Cclass _) => 1
-  | (Cptr_to_fld fn1 t1, Cptr_to_fld fn2 t2) =>
-    let n = Ident.fieldname_compare fn1 fn2;
-    if (n != 0) {
-      n
-    } else {
-      Typ.compare t1 t2
-    }
-  };
-
-let const_equal c1 c2 => const_compare c1 c2 == 0;
-
-let const_kind_equal c1 c2 => {
-  let const_kind_number =
-    fun
-    | Cint _ => 1
-    | Cfun _ => 2
-    | Cstr _ => 3
-    | Cfloat _ => 4
-    | Cclass _ => 5
-    | Cptr_to_fld _ => 6;
-  const_kind_number c1 == const_kind_number c2
-};
-
 let rec dexp_has_tmp_var =
   fun
   | Dpvar pvar
@@ -1168,7 +1117,7 @@ let rec exp_compare (e1: exp) (e2: exp) :int =>
     }
   | (Closure _, _) => (-1)
   | (_, Closure _) => 1
-  | (Const c1, Const c2) => const_compare c1 c2
+  | (Const c1, Const c2) => Const.compare c1 c2
   | (Const _, _) => (-1)
   | (_, Const _) => 1
   | (Cast t1 e1, Cast t2 e2) =>
@@ -1594,19 +1543,6 @@ let java () => !Config.curr_language == Config.Java;
 
 let eradicate_java () => Config.eradicate && java ();
 
-let pp_const pe f =>
-  fun
-  | Cint i => IntLit.pp f i
-  | Cfun fn =>
-    switch pe.pe_kind {
-    | PP_HTML => F.fprintf f "_fun_%s" (Escape.escape_xml (Procname.to_string fn))
-    | _ => F.fprintf f "_fun_%s" (Procname.to_string fn)
-    }
-  | Cstr s => F.fprintf f "\"%s\"" (String.escaped s)
-  | Cfloat v => F.fprintf f "%f" v
-  | Cclass c => F.fprintf f "%a" Ident.pp_name c
-  | Cptr_to_fld fn _ => F.fprintf f "__fld_%a" Ident.pp_fieldname fn;
-
 
 /** convert a dexp to a string */
 let rec dexp_to_string =
@@ -1614,7 +1550,7 @@ let rec dexp_to_string =
   | Darray de1 de2 => dexp_to_string de1 ^ "[" ^ dexp_to_string de2 ^ "]"
   | Dbinop op de1 de2 => "(" ^ dexp_to_string de1 ^ str_binop pe_text op ^ dexp_to_string de2 ^ ")"
   | Dconst (Cfun pn) => Procname.to_simplified_string pn
-  | Dconst c => pp_to_string (pp_const pe_text) c
+  | Dconst c => Const.to_string c
   | Dderef de => "*" ^ dexp_to_string de
   | Dfcall fun_dexp args _ {cf_virtual: isvirtual} => {
       let pp_arg fmt de => F.fprintf fmt "%s" (dexp_to_string de);
@@ -1818,7 +1754,7 @@ let rec _pp_exp pe0 pp_t f e0 => {
       };
     switch e {
     | Var id => (Ident.pp pe) f id
-    | Const c => F.fprintf f "%a" (pp_const pe) c
+    | Const c => F.fprintf f "%a" (Const.pp pe) c
     | Cast typ e => F.fprintf f "(%a)%a" pp_t typ pp_exp e
     | UnOp op e _ => F.fprintf f "%s%a" (str_unop op) pp_exp e
     | BinOp op (Const c) e2 when Config.smt_output => print_binop_stm_output (Const c) op e2
diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei
index 1f77b99c2..dd9b151bd 100644
--- a/infer/src/IR/Sil.rei
+++ b/infer/src/IR/Sil.rei
@@ -142,22 +142,11 @@ type taint_kind =
 type taint_info = {taint_source: Procname.t, taint_kind: taint_kind};
 
 
-/** Constants */
-type const =
-  | Cint of IntLit.t /** integer constants */
-  | Cfun of Procname.t /** function names */
-  | Cstr of string /** string constants */
-  | Cfloat of float /** float constants */
-  | Cclass of Ident.name /** class constant */
-  | Cptr_to_fld of Ident.fieldname Typ.t /** pointer to field constant,
-                                             and type of the surrounding Csu.t type */;
-
-
 /** expression representing the result of decompilation */
 type dexp =
   | Darray of dexp dexp
   | Dbinop of binop dexp dexp
-  | Dconst of const
+  | Dconst of Const.t
   | Dsizeof of Typ.t (option dexp) Subtype.t
   | Dderef of dexp
   | Dfcall of dexp (list dexp) Location.t call_flags
@@ -223,7 +212,7 @@ and exp =
   /** Anonymous function */
   | Closure of closure
   /** Constants */
-  | Const of const
+  | Const of Const.t
   /** Type cast */
   | Cast of Typ.t exp
   /** The address of a program variable */
@@ -559,14 +548,6 @@ let attribute_to_category: attribute => attribute_category;
 
 let attr_is_undef: attribute => bool;
 
-let const_compare: const => const => int;
-
-let const_equal: const => const => bool;
-
-
-/** Return true if the constants have the same kind (both integers, ...) */
-let const_kind_equal: const => const => bool;
-
 let exp_compare: exp => exp => int;
 
 let exp_equal: exp => exp => bool;
@@ -656,10 +637,6 @@ let mem_alloc_pname: mem_kind => Procname.t;
 let mem_dealloc_pname: mem_kind => Procname.t;
 
 
-/** Pretty print a const. */
-let pp_const: printenv => F.formatter => const => unit;
-
-
 /** convert the attribute to a string */
 let attribute_to_string: printenv => attribute => string;
 
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index 2f0b57752..d8d415ecd 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -778,10 +778,10 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) =
            match a with
            | Sil.Aneq (Sil.Var _, _) -> a:: pi
            (* we only use Lt and Le because Gt and Ge are inserted in terms of Lt and Le. *)
-           | Sil.Aeq (Sil.Const (Sil.Cint i), Sil.BinOp (Sil.Lt, _, _))
-           | Sil.Aeq (Sil.BinOp (Sil.Lt, _, _), Sil.Const (Sil.Cint i))
-           | Sil.Aeq (Sil.Const (Sil.Cint i), Sil.BinOp (Sil.Le, _, _))
-           | Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
+           | Sil.Aeq (Sil.Const (Const.Cint i), Sil.BinOp (Sil.Lt, _, _))
+           | Sil.Aeq (Sil.BinOp (Sil.Lt, _, _), Sil.Const (Const.Cint i))
+           | Sil.Aeq (Sil.Const (Const.Cint i), Sil.BinOp (Sil.Le, _, _))
+           | Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Const.Cint i)) when IntLit.isone i ->
                a :: pi
            | Sil.Aeq (Sil.Var name, e) when not (Ident.is_primed name) ->
                (match e with
@@ -929,7 +929,7 @@ let get_cycle root prop =
 (* specified buckets. In the positive case, it returns the bucket *)
 let should_raise_objc_leak hpred =
   match hpred with
-  | Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Sil.Const (Sil.Cint i)), _)):: _, _),
+  | Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Sil.Const (Const.Cint i)), _)):: _, _),
                   Sil.Sizeof (typ, _, _))
     when Ident.fieldname_is_hidden fn && IntLit.gt i IntLit.zero (* counter > 0 *) ->
       Mleak_buckets.should_raise_objc_leak typ
diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml
index cf4efe05a..757023676 100644
--- a/infer/src/backend/absarray.ml
+++ b/infer/src/backend/absarray.ml
@@ -581,7 +581,7 @@ let remove_redundant_elements prop =
       modified := true;
       false in
     match e, se with
-    | Sil.Const (Sil.Cint i), Sil.Eexp (Sil.Var id, _)
+    | Sil.Const (Const.Cint i), Sil.Eexp (Sil.Var id, _)
       when (not fp_part || IntLit.iszero i) && not (Ident.is_normal id) && occurs_at_most_once id ->
         remove () (* unknown value can be removed in re-execution mode or if the index is zero *)
     | Sil.Var id, Sil.Eexp _ when Ident.is_normal id = false && occurs_at_most_once id ->
diff --git a/infer/src/backend/autounit.ml b/infer/src/backend/autounit.ml
index 76d713c7c..f12b08821 100644
--- a/infer/src/backend/autounit.ml
+++ b/infer/src/backend/autounit.ml
@@ -184,9 +184,9 @@ end = struct
 
   let rec pi_iter do_le do_lt do_neq pi =
     let do_atom a = match a with
-      | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
+      | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Const.Cint i)) when IntLit.isone i ->
           do_le e1 e2
-      | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
+      | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Const.Cint i)) when IntLit.isone i ->
           do_lt e1 e2
       | Sil.Aeq _ -> ()
       | Sil.Aneq (e1, e2) ->
@@ -217,33 +217,33 @@ end = struct
       | Some n1, Some n2 -> Some (IntLit.sub n1 n2)
       | _ -> None in
     let do_le e1 e2 = match e1, e2 with
-      | Sil.Var id, Sil.Const (Sil.Cint n) ->
+      | Sil.Var id, Sil.Const (Const.Cint n) ->
           let rng = IdMap.find id ev in
           add_top rng id n
-      | Sil.BinOp (Sil.MinusA, Sil.Var id1, Sil.Var id2), Sil.Const (Sil.Cint n) ->
+      | Sil.BinOp (Sil.MinusA, Sil.Var id1, Sil.Var id2), Sil.Const (Const.Cint n) ->
           let rng1 = IdMap.find id1 ev in
           let rng2 = IdMap.find id2 ev in
           update_top rng1 id1 (rng2.top +++ (Some n));
           update_bottom rng2 id2 (rng1.bottom --- (Some n))
-      | Sil.BinOp (Sil.PlusA, Sil.Var id1, Sil.Var id2), Sil.Const (Sil.Cint n) ->
+      | Sil.BinOp (Sil.PlusA, Sil.Var id1, Sil.Var id2), Sil.Const (Const.Cint n) ->
           let rng1 = IdMap.find id1 ev in
           let rng2 = IdMap.find id2 ev in
           update_top rng1 id1 (Some n --- rng2.bottom);
           update_top rng2 id2 (Some n --- rng1.bottom)
       | _ -> if debug then assert false in
     let do_lt e1 e2 = match e1, e2 with
-      | Sil.Const (Sil.Cint n), Sil.Var id ->
+      | Sil.Const (Const.Cint n), Sil.Var id ->
           let rng = IdMap.find id ev in
           add_bottom rng id (n ++ IntLit.one)
-      | Sil.Const (Sil.Cint n), Sil.BinOp (Sil.PlusA, Sil.Var id1, Sil.Var id2) ->
+      | Sil.Const (Const.Cint n), Sil.BinOp (Sil.PlusA, Sil.Var id1, Sil.Var id2) ->
           let rng1 = IdMap.find id1 ev in
           let rng2 = IdMap.find id2 ev in
           update_bottom rng1 id1 (Some (n ++ IntLit.one) --- rng2.top);
           update_bottom rng2 id2 (Some (n ++ IntLit.one) --- rng1.top)
       | _ -> if debug then assert false in
     let rec do_neq e1 e2 = match e1, e2 with
-      | Sil.Var id, Sil.Const (Sil.Cint n)
-      | Sil.Const(Sil.Cint n), Sil.Var id ->
+      | Sil.Var id, Sil.Const (Const.Cint n)
+      | Sil.Const(Const.Cint n), Sil.Var id ->
           let rng = IdMap.find id ev in
           add_excluded rng id n
       | Sil.Var id1, Sil.Var id2 ->
@@ -254,7 +254,7 @@ end = struct
                do_neq (Sil.exp_int n1) e2
            | None, Some n2 ->
                do_neq e1 (Sil.exp_int n2))
-      | Sil.Var id1, Sil.BinOp(Sil.PlusA, Sil.Var id2, Sil.Const (Sil.Cint n)) ->
+      | Sil.Var id1, Sil.BinOp(Sil.PlusA, Sil.Var id2, Sil.Const (Const.Cint n)) ->
           (match solved ev id1, solved ev id2 with
            | None, None -> ()
            | Some _, Some _ -> ()
@@ -513,19 +513,19 @@ let gen_var_decl code idmap parameters =
 (** initialize variables not requiring allocation *)
 let gen_init_vars code solutions idmap =
   let get_const id c =
-    try Sil.Cint (IdMap.find id solutions)
+    try Const.Cint (IdMap.find id solutions)
     with Not_found -> c in
   let do_vinfo id { typ = typ; alloc = alloc } =
     if not alloc then
       let const = match typ with
         | Typ.Tint _ | Typ.Tvoid ->
-            get_const id (Sil.Cint IntLit.zero)
+            get_const id (Const.Cint IntLit.zero)
         | Typ.Tfloat _ ->
-            Sil.Cfloat 0.0
+            Const.Cfloat 0.0
         | Typ.Tptr _ ->
-            get_const id (Sil.Cint IntLit.zero)
+            get_const id (Const.Cint IntLit.zero)
         | Typ.Tfun _ ->
-            Sil.Cint IntLit.zero
+            Const.Cint IntLit.zero
         | typ ->
             L.err "do_vinfo type undefined: %a@." (Typ.pp_full pe) typ;
             assert false in
diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml
index 298c811af..fdc5a5ba8 100644
--- a/infer/src/backend/buckets.ml
+++ b/infer/src/backend/buckets.ml
@@ -72,13 +72,13 @@ let check_access access_opt de_opt =
     let formal_param_used_in_call = ref false in
     let has_call_or_sets_null node =
       let rec exp_is_null exp = match exp with
-        | Sil.Const (Sil.Cint n) -> IntLit.iszero n
+        | Sil.Const (Const.Cint n) -> IntLit.iszero n
         | Sil.Cast (_, e) -> exp_is_null e
         | Sil.Var _
         | Sil.Lvar _ ->
             begin
               match State.get_const_map () node exp with
-              | Some (Sil.Cint n) ->
+              | Some (Const.Cint n) ->
                   IntLit.iszero n
               | _ -> false
             end
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index f517f4a8e..0671a8d29 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -473,7 +473,7 @@ end = struct
 
     let add_and_chk_eq e1 e1' n =
       match e1, e1' with
-      | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n1') -> IntLit.eq (n1 ++ n) n1'
+      | Sil.Const (Const.Cint n1), Sil.Const (Const.Cint n1') -> IntLit.eq (n1 ++ n) n1'
       | _ -> false in
     let add_and_gen_eq e e' n =
       let e_plus_n = Sil.BinOp(Sil.PlusA, e, Sil.exp_int n) in
@@ -499,7 +499,7 @@ end = struct
 
     let f_ineqs acc (e1, e2, e) =
       match e1, e2 with
-      | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) ->
+      | Sil.Const (Const.Cint n1), Sil.Const (Const.Cint n2) ->
           let strict_lower1, upper1 =
             if IntLit.leq n1 n2 then (n1 -- IntLit.one, n2) else (n2 -- IntLit.one, n1) in
           let e_strict_lower1 = Sil.exp_int strict_lower1 in
@@ -591,12 +591,12 @@ end = struct
   let lookup_side_induced' side e =
     let res = ref [] in
     let f v = match v, side with
-      | (Sil.BinOp (Sil.PlusA, e1', Sil.Const (Sil.Cint i)), e2, e'), Lhs
+      | (Sil.BinOp (Sil.PlusA, e1', Sil.Const (Const.Cint i)), e2, e'), Lhs
         when Sil.exp_equal e e1' ->
           let c' = Sil.exp_int (IntLit.neg i) in
           let v' = (e1', Sil.BinOp(Sil.PlusA, e2, c'), Sil.BinOp (Sil.PlusA, e', c')) in
           res := v'::!res
-      | (e1, Sil.BinOp (Sil.PlusA, e2', Sil.Const (Sil.Cint i)), e'), Rhs
+      | (e1, Sil.BinOp (Sil.PlusA, e2', Sil.Const (Const.Cint i)), e'), Rhs
         when Sil.exp_equal e e2' ->
           let c' = Sil.exp_int (IntLit.neg i) in
           let v' = (Sil.BinOp(Sil.PlusA, e1, c'), e2', Sil.BinOp (Sil.PlusA, e', c')) in
@@ -722,14 +722,14 @@ end = struct
           when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
             build_other_atoms (fun e0 -> Prop.mk_eq e0 e') side e
 
-        | Sil.Aeq(Sil.BinOp(Sil.Le, e, e'), Sil.Const (Sil.Cint i))
-        | Sil.Aeq(Sil.Const (Sil.Cint i), Sil.BinOp(Sil.Le, e, e'))
+        | Sil.Aeq(Sil.BinOp(Sil.Le, e, e'), Sil.Const (Const.Cint i))
+        | Sil.Aeq(Sil.Const (Const.Cint i), Sil.BinOp(Sil.Le, e, e'))
           when IntLit.isone i && (exp_contains_only_normal_ids e') ->
             let construct e0 = Prop.mk_inequality (Sil.BinOp(Sil.Le, e0, e')) in
             build_other_atoms construct side e
 
-        | Sil.Aeq(Sil.BinOp(Sil.Lt, e', e), Sil.Const (Sil.Cint i))
-        | Sil.Aeq(Sil.Const (Sil.Cint i), Sil.BinOp(Sil.Lt, e', e))
+        | Sil.Aeq(Sil.BinOp(Sil.Lt, e', e), Sil.Const (Const.Cint i))
+        | Sil.Aeq(Sil.Const (Const.Cint i), Sil.BinOp(Sil.Lt, e', e))
           when IntLit.isone i && (exp_contains_only_normal_ids e') ->
             let construct e0 = Prop.mk_inequality (Sil.BinOp(Sil.Lt, e', e0)) in
             build_other_atoms construct side e
@@ -889,9 +889,9 @@ let option_partial_join partial_join o1 o2 =
   | Some x1, Some x2 -> partial_join x1 x2
 
 let const_partial_join c1 c2 =
-  let is_int = function Sil.Cint _ -> true | _ -> false in
-  if Sil.const_equal c1 c2 then Sil.Const c1
-  else if Sil.const_kind_equal c1 c2 && not (is_int c1) then
+  let is_int = function Const.Cint _ -> true | _ -> false in
+  if Const.equal c1 c2 then Sil.Const c1
+  else if Const.kind_equal c1 c2 && not (is_int c1) then
     (L.d_strln "failure reason 18"; raise IList.Fail)
   else if !Config.abs_val >= 2 then
     FreshVarExp.get_fresh_exp (Sil.Const c1) (Sil.Const c2)
@@ -921,12 +921,12 @@ let rec exp_partial_join (e1: Sil.exp) (e2: Sil.exp) : Sil.exp =
   | Sil.Var id1, Sil.BinOp(Sil.PlusA, Sil.Var id2, Sil.Const _)
     when ident_same_kind_primed_footprint id1 id2 ->
       Rename.extend e1 e2 Rename.ExtFresh
-  | Sil.BinOp(Sil.PlusA, Sil.Var id1, Sil.Const (Sil.Cint c1)), Sil.Const (Sil.Cint c2)
+  | Sil.BinOp(Sil.PlusA, Sil.Var id1, Sil.Const (Const.Cint c1)), Sil.Const (Const.Cint c2)
     when can_rename id1 ->
       let c2' = c2 -- c1 in
       let e_res = Rename.extend (Sil.Var id1) (Sil.exp_int c2') Rename.ExtFresh in
       Sil.BinOp(Sil.PlusA, e_res, Sil.exp_int c1)
-  | Sil.Const (Sil.Cint c1), Sil.BinOp(Sil.PlusA, Sil.Var id2, Sil.Const (Sil.Cint c2))
+  | Sil.Const (Const.Cint c1), Sil.BinOp(Sil.PlusA, Sil.Var id2, Sil.Const (Const.Cint c2))
     when can_rename id2 ->
       let c1' = c1 -- c2 in
       let e_res = Rename.extend (Sil.exp_int c1') (Sil.Var id2) Rename.ExtFresh in
@@ -1011,7 +1011,7 @@ let rec exp_partial_meet (e1: Sil.exp) (e2: Sil.exp) : Sil.exp =
         Rename.extend e1 e2 (Rename.ExtDefault(e1))
       else (L.d_strln "failure reason 28"; raise IList.Fail)
   | Sil.Const c1, Sil.Const c2 ->
-      if (Sil.const_equal c1 c2) then e1 else (L.d_strln "failure reason 29"; raise IList.Fail)
+      if (Const.equal c1 c2) then e1 else (L.d_strln "failure reason 29"; raise IList.Fail)
   | Sil.Cast(t1, e1), Sil.Cast(t2, e2) ->
       if not (Typ.equal t1 t2) then (L.d_strln "failure reason 30"; raise IList.Fail)
       else
@@ -1575,7 +1575,7 @@ let pi_partial_join mode
     (* find some array length in the prop, to be used as heuritic for upper bound in widening *)
     let len_list = ref [] in
     let do_hpred = function
-      | Sil.Hpointsto (_, Sil.Earray (Sil.Const (Sil.Cint n), _, _), _) ->
+      | Sil.Hpointsto (_, Sil.Earray (Sil.Const (Const.Cint n), _, _), _) ->
           (if IntLit.geq n IntLit.one then len_list := n :: !len_list)
       | _ -> () in
     IList.iter do_hpred (Prop.get_sigma prop);
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index 5abf03b3e..50cb199ae 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -327,7 +327,7 @@ let rec dotty_mk_node pe sigma =
 
 let set_exps_neq_zero pi =
   let f = function
-    | Sil.Aneq (e, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
+    | Sil.Aneq (e, Sil.Const (Const.Cint i)) when IntLit.iszero i ->
         exps_neq_zero := e :: !exps_neq_zero
     | _ -> () in
   exps_neq_zero := [];
diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml
index 0e73c8a4a..64540772c 100644
--- a/infer/src/backend/errdesc.ml
+++ b/infer/src/backend/errdesc.ml
@@ -73,7 +73,7 @@ let explain_deallocate_stack_var pvar ra =
 let explain_deallocate_constant_string s ra =
   let const_str =
     let pp fmt () =
-      Sil.pp_exp pe_text fmt (Sil.Const (Sil.Cstr s)) in
+      Sil.pp_exp pe_text fmt (Sil.Const (Const.Cstr s)) in
     pp_to_string pp () in
   Localise.desc_deallocate_static_memory const_str ra.Sil.ra_pname ra.Sil.ra_loc
 
@@ -203,7 +203,7 @@ let find_ident_assignment node id : (Cfg.Node.t * Sil.exp) option =
 let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option =
   let find_instr n =
     let filter = function
-      | Sil.Set (Sil.Lvar _pvar, _, Sil.Const (Sil.Cint i), _) when Pvar.equal pvar _pvar ->
+      | Sil.Set (Sil.Lvar _pvar, _, Sil.Const (Const.Cint i), _) when Pvar.equal pvar _pvar ->
           IntLit.iszero i <> true_branch
       | _ -> false in
     IList.exists filter (Cfg.Node.get_instrs n) in
@@ -226,21 +226,21 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
           (L.d_str "find_normal_variable_letderef defining ";
            Sil.d_exp e; L.d_ln ());
         _exp_lv_dexp seen node e
-    | Sil.Call ([id0], Sil.Const (Sil.Cfun pn), (e, _):: _, _, _)
+    | Sil.Call ([id0], Sil.Const (Const.Cfun pn), (e, _):: _, _, _)
       when Ident.equal id id0 && Procname.equal pn (Procname.from_string_c_fun "__cast") ->
         if verbose
         then
           (L.d_str "find_normal_variable_letderef cast on ";
            Sil.d_exp e; L.d_ln ());
         _exp_rv_dexp seen node e
-    | Sil.Call ([id0], (Sil.Const (Sil.Cfun pname) as fun_exp), args, loc, call_flags)
+    | Sil.Call ([id0], (Sil.Const (Const.Cfun pname) as fun_exp), args, loc, call_flags)
       when Ident.equal id id0 ->
         if verbose
         then
           (L.d_str "find_normal_variable_letderef function call ";
            Sil.d_exp fun_exp; L.d_ln ());
 
-        let fun_dexp = Sil.Dconst (Sil.Cfun pname) in
+        let fun_dexp = Sil.Dconst (Const.Cfun pname) in
         let args_dexp =
           let args_dexpo = IList.map (fun (e, _) -> _exp_rv_dexp seen node e) args in
           if IList.exists (fun x -> x = None) args_dexpo
@@ -760,10 +760,10 @@ let explain_dexp_access prop dexp is_nullable =
     | Sil.Dfcall (Sil.Dconst c, _, loc, _) ->
         if verbose then (L.d_strln "lookup: found Dfcall ");
         (match c with
-         | Sil.Cfun _ -> (* Treat function as an update *)
+         | Const.Cfun _ -> (* Treat function as an update *)
              Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_call loc.Location.line))
          | _ -> None)
-    | Sil.Dretcall (Sil.Dconst (Sil.Cfun pname as c ) , _, loc, _ )
+    | Sil.Dretcall (Sil.Dconst (Const.Cfun pname as c ) , _, loc, _ )
       when method_of_pointer_wrapper pname ->
         if verbose then (L.d_strln "lookup: found Dretcall ");
         Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_pointer_wrapper_call loc.Location.line))
@@ -920,7 +920,7 @@ let _explain_access
     | Some Sil.Letderef (_, e, _, _) ->
         if verbose then (L.d_str "explain_dereference Sil.Leteref "; Sil.d_exp e; L.d_ln ());
         Some e
-    | Some Sil.Call (_, Sil.Const (Sil.Cfun fn), [(e, _)], _, _)
+    | Some Sil.Call (_, Sil.Const (Const.Cfun fn), [(e, _)], _, _)
       when Procname.to_string fn = "free" ->
         if verbose then (L.d_str "explain_dereference Sil.Call "; Sil.d_exp e; L.d_ln ());
         Some e
diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml
index 940cbd62a..8c81e94e6 100644
--- a/infer/src/backend/match.ml
+++ b/infer/src/backend/match.ml
@@ -719,7 +719,7 @@ let sigma_lift_to_pe sigma =
 let generic_para_create corres sigma1 elist1 =
   let corres_ids =
     let not_same_consts = function
-      | Sil.Const c1, Sil.Const c2 -> not (Sil.const_equal c1 c2)
+      | Sil.Const c1, Sil.Const c2 -> not (Const.equal c1 c2)
       | _ -> true in
     let new_corres' = IList.filter not_same_consts corres in
     let add_fresh_id pair = (pair, Ident.create_fresh Ident.kprimed) in
diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml
index 8982defe7..273c99705 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/modelBuiltins.ml
@@ -480,7 +480,7 @@ let execute___objc_counter_update
         Sil.Set
           (hidden_field,
            typ',
-           Sil.BinOp(op, Sil.Var tmp, Sil.Const (Sil.Cint delta)),
+           Sil.BinOp(op, Sil.Var tmp, Sil.Const (Const.Cint delta)),
            loc) in
       let update_counter_instrs =
         [ counter_to_tmp; update_counter; Sil.Remove_temps([tmp], loc) ] in
@@ -492,7 +492,7 @@ let execute___objc_counter_update
    removed from the list of args. *)
 let get_suppress_npe_flag args =
   match args with
-  | (Sil.Const (Sil.Cint i), Typ.Tint Typ.IBool):: args' when IntLit.isone i ->
+  | (Sil.Const (Const.Cint i), Typ.Tint Typ.IBool):: args' when IntLit.isone i ->
       false, args' (* this is a CFRelease/CFRetain *)
   | _ -> true, args
 
@@ -631,7 +631,7 @@ let execute___set_taint_attribute
     ({ Builtin.pdesc; args; prop_; path; })
   : Builtin.ret_typ =
   match args with
-  | (exp, _) :: [(Sil.Const (Sil.Cstr taint_kind_str), _)] ->
+  | (exp, _) :: [(Sil.Const (Const.Cstr taint_kind_str), _)] ->
       let taint_source = Cfg.Procdesc.get_proc_name pdesc in
       let taint_kind = match taint_kind_str with
         | "UnverifiedSSLSocket" -> Sil.Tk_unverified_SSL_socket
@@ -762,7 +762,7 @@ let execute_alloc mk can_return_null
     | Sil.Sizeof (Typ.Tarray (Typ.Tint ik, _), Some len, _) when Typ.ikind_is_char ik ->
         evaluate_char_sizeof len
     | Sil.Sizeof (Typ.Tarray (Typ.Tint ik, Some len), None, _) when Typ.ikind_is_char ik ->
-        evaluate_char_sizeof (Sil.Const (Sil.Cint len))
+        evaluate_char_sizeof (Sil.Const (Const.Cint len))
     | Sil.Sizeof _ -> e
     | Sil.Attribute _ -> e in
   let size_exp, procname = match args with
@@ -776,7 +776,7 @@ let execute_alloc mk can_return_null
         Sil.Sizeof (struct_type, len, subt), pname
     | [(size_exp, _)] -> (* for malloc and __new *)
         size_exp, Sil.mem_alloc_pname mk
-    | [(size_exp, _); (Sil.Const (Sil.Cfun pname), _)] ->
+    | [(size_exp, _); (Sil.Const (Const.Cfun pname), _)] ->
         size_exp, pname
     | _ ->
         raise (Exceptions.Wrong_argument_number __POS__) in
@@ -828,7 +828,7 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r)
                | _ -> typ
              with Not_found -> typ in
            let typ_string = Typ.to_string typ in
-           let set_instr = Sil.Set (field_exp, Typ.Tvoid, Sil.Const (Sil.Cstr typ_string), loc) in
+           let set_instr = Sil.Set (field_exp, Typ.Tvoid, Sil.Const (Const.Cstr typ_string), loc) in
            SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] res
        | _ -> res)
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@@ -907,12 +907,12 @@ let execute___split_get_nth { Builtin.pdesc; prop_; path; ret_ids; args; }
       let n_lexp2, prop___ = check_arith_norm_exp pname lexp2 prop__ in
       let n_lexp3, prop = check_arith_norm_exp pname lexp3 prop___ in
       (match n_lexp1, n_lexp2, n_lexp3 with
-       | Sil.Const (Sil.Cstr str1), Sil.Const (Sil.Cstr str2), Sil.Const (Sil.Cint n_sil) ->
+       | Sil.Const (Const.Cstr str1), Sil.Const (Const.Cstr str2), Sil.Const (Const.Cint n_sil) ->
            (let n = IntLit.to_int n_sil in
             try
               let parts = Str.split (Str.regexp_string str2) str1 in
               let n_part = IList.nth parts n in
-              let res = Sil.Const (Sil.Cstr n_part) in
+              let res = Sil.Const (Const.Cstr n_part) in
               [(return_result res prop ret_ids, path)]
             with Not_found -> assert false)
        | _ -> [(prop, path)])
@@ -938,13 +938,13 @@ let execute___infer_fail { Builtin.pdesc; tenv; prop_; path; args; loc; }
     | [(lexp_msg, _)] ->
         begin
           match Prop.exp_normalize_prop prop_ lexp_msg with
-          | Sil.Const (Sil.Cstr str) -> str
+          | Sil.Const (Const.Cstr str) -> str
           | _ -> assert false
         end
     | _ ->
         raise (Exceptions.Wrong_argument_number __POS__) in
   let set_instr =
-    Sil.Set (Sil.Lvar Sil.custom_error, Typ.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in
+    Sil.Set (Sil.Lvar Sil.custom_error, Typ.Tvoid, Sil.Const (Const.Cstr error_str), loc) in
   SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)]
 
 (* translate builtin assertion failure *)
@@ -957,7 +957,7 @@ let execute___assert_fail { Builtin.pdesc; tenv; prop_; path; args; loc; }
     | _ ->
         raise (Exceptions.Wrong_argument_number __POS__) in
   let set_instr =
-    Sil.Set (Sil.Lvar Sil.custom_error, Typ.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in
+    Sil.Set (Sil.Lvar Sil.custom_error, Typ.Tvoid, Sil.Const (Const.Cstr error_str), loc) in
   SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)]
 
 let __assert_fail = Builtin.register
@@ -1157,12 +1157,12 @@ let _ = Builtin.register
 let execute_objc_alloc_no_fail
     symb_state typ alloc_fun_opt
     { Builtin.pdesc; tenv; ret_ids; loc; } =
-  let alloc_fun = Sil.Const (Sil.Cfun __objc_alloc_no_fail) in
+  let alloc_fun = Sil.Const (Const.Cfun __objc_alloc_no_fail) in
   let ptr_typ = Typ.Tptr (typ, Typ.Pk_pointer) in
   let sizeof_typ = Sil.Sizeof (typ, None, Sil.Subtype.exact) in
   let alloc_fun_exp =
     match alloc_fun_opt with
-    | Some pname -> [Sil.Const (Sil.Cfun pname), Typ.Tvoid]
+    | Some pname -> [Sil.Const (Const.Cfun pname), Typ.Tvoid]
     | None -> [] in
   let alloc_instr =
     Sil.Call (ret_ids, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, Sil.cf_default) in
diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml
index f93ba28fd..69276f9df 100644
--- a/infer/src/backend/preanal.ml
+++ b/infer/src/backend/preanal.ml
@@ -24,7 +24,7 @@ let add_dispatch_calls pdesc cg tenv =
     let has_dispatch_call instrs =
       IList.exists instr_is_dispatch_call instrs in
     let replace_dispatch_calls = function
-      | Sil.Call (ret_ids, (Sil.Const (Sil.Cfun callee_pname) as call_exp),
+      | Sil.Call (ret_ids, (Sil.Const (Const.Cfun callee_pname) as call_exp),
                   (((_, receiver_typ) :: _) as args), loc, call_flags) as instr
         when call_flags_is_dispatch call_flags ->
           (* the frontend should not populate the list of targets *)
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index 369e02a3e..803ec9214 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -430,18 +430,18 @@ let (--) = IntLit.sub
 let (++) = IntLit.add
 
 let iszero_int_float = function
-  | Sil.Cint i -> IntLit.iszero i
-  | Sil.Cfloat 0.0 -> true
+  | Const.Cint i -> IntLit.iszero i
+  | Const.Cfloat 0.0 -> true
   | _ -> false
 
 let isone_int_float = function
-  | Sil.Cint i -> IntLit.isone i
-  | Sil.Cfloat 1.0 -> true
+  | Const.Cint i -> IntLit.isone i
+  | Const.Cfloat 1.0 -> true
   | _ -> false
 
 let isminusone_int_float = function
-  | Sil.Cint i -> IntLit.isminusone i
-  | Sil.Cfloat (-1.0) -> true
+  | Const.Cint i -> IntLit.isminusone i
+  | Const.Cfloat (-1.0) -> true
   | _ -> false
 
 let sym_eval abs e =
@@ -461,7 +461,7 @@ let sym_eval abs e =
         eval l
     | Sil.Sizeof (Typ.Tarray (Typ.Tint ik, Some l), _, _)
       when Typ.ikind_is_char ik && !Config.curr_language = Config.Clang ->
-        Sil.Const (Sil.Cint l)
+        Sil.Const (Const.Cint l)
     | Sil.Sizeof _ ->
         e
     | Sil.Cast (_, e1) ->
@@ -469,9 +469,9 @@ let sym_eval abs e =
     | Sil.UnOp (Sil.LNot, e1, topt) ->
         begin
           match eval e1 with
-          | Sil.Const (Sil.Cint i) when IntLit.iszero i ->
+          | Sil.Const (Const.Cint i) when IntLit.iszero i ->
               Sil.exp_one
-          | Sil.Const (Sil.Cint _) ->
+          | Sil.Const (Const.Cint _) ->
               Sil.exp_zero
           | Sil.UnOp(Sil.LNot, e1', _) ->
               e1'
@@ -483,9 +483,9 @@ let sym_eval abs e =
           match eval e1 with
           | Sil.UnOp (Sil.Neg, e2', _) ->
               e2'
-          | Sil.Const (Sil.Cint i) ->
+          | Sil.Const (Const.Cint i) ->
               Sil.exp_int (IntLit.neg i)
-          | Sil.Const (Sil.Cfloat v) ->
+          | Sil.Const (Const.Cfloat v) ->
               Sil.exp_float (-. v)
           | Sil.Var id ->
               Sil.UnOp (Sil.Neg, Sil.Var id, topt)
@@ -497,7 +497,7 @@ let sym_eval abs e =
           match eval e1 with
           | Sil.UnOp(Sil.BNot, e2', _) ->
               e2'
-          | Sil.Const (Sil.Cint i) ->
+          | Sil.Const (Const.Cint i) ->
               Sil.exp_int (IntLit.lognot i)
           | e1' ->
               if abs then Sil.exp_get_undefined false else Sil.UnOp (Sil.BNot, e1', topt)
@@ -505,11 +505,11 @@ let sym_eval abs e =
     | Sil.BinOp (Sil.Le, e1, e2) ->
         begin
           match eval e1, eval e2 with
-          | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
+          | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) ->
               Sil.exp_bool (IntLit.leq n m)
-          | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
+          | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) ->
               Sil.exp_bool (v <= w)
-          | Sil.BinOp (Sil.PlusA, e3, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint m) ->
+          | Sil.BinOp (Sil.PlusA, e3, Sil.Const (Const.Cint n)), Sil.Const (Const.Cint m) ->
               Sil.BinOp (Sil.Le, e3, Sil.exp_int (m -- n))
           | e1', e2' ->
               Sil.exp_le e1' e2'
@@ -517,16 +517,16 @@ let sym_eval abs e =
     | Sil.BinOp (Sil.Lt, e1, e2) ->
         begin
           match eval e1, eval e2 with
-          | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
+          | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) ->
               Sil.exp_bool (IntLit.lt n m)
-          | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
+          | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) ->
               Sil.exp_bool (v < w)
-          | Sil.Const (Sil.Cint n), Sil.BinOp (Sil.MinusA, f1, f2) ->
+          | Sil.Const (Const.Cint n), Sil.BinOp (Sil.MinusA, f1, f2) ->
               Sil.BinOp
                 (Sil.Le, Sil.BinOp (Sil.MinusA, f2, f1), Sil.exp_int (IntLit.minus_one -- n))
-          | Sil.BinOp(Sil.MinusA, f1 , f2), Sil.Const(Sil.Cint n) ->
+          | Sil.BinOp(Sil.MinusA, f1 , f2), Sil.Const(Const.Cint n) ->
               Sil.exp_le (Sil.BinOp(Sil.MinusA, f1 , f2)) (Sil.exp_int (n -- IntLit.one))
-          | Sil.BinOp (Sil.PlusA, e3, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint m) ->
+          | Sil.BinOp (Sil.PlusA, e3, Sil.Const (Const.Cint n)), Sil.Const (Const.Cint m) ->
               Sil.BinOp (Sil.Lt, e3, Sil.exp_int (m -- n))
           | e1', e2' ->
               Sil.exp_lt e1' e2'
@@ -538,9 +538,9 @@ let sym_eval abs e =
     | Sil.BinOp (Sil.Eq, e1, e2) ->
         begin
           match eval e1, eval e2 with
-          | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
+          | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) ->
               Sil.exp_bool (IntLit.eq n m)
-          | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
+          | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) ->
               Sil.exp_bool (v = w)
           | e1', e2' ->
               Sil.exp_eq e1' e2'
@@ -548,9 +548,9 @@ let sym_eval abs e =
     | Sil.BinOp (Sil.Ne, e1, e2) ->
         begin
           match eval e1, eval e2 with
-          | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
+          | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) ->
               Sil.exp_bool (IntLit.neq n m)
-          | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
+          | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) ->
               Sil.exp_bool (v <> w)
           | e1', e2' ->
               Sil.exp_ne e1' e2'
@@ -559,13 +559,13 @@ let sym_eval abs e =
         let e1' = eval e1 in
         let e2' = eval e2 in
         begin match e1', e2' with
-          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
+          | Sil.Const (Const.Cint i), _ when IntLit.iszero i ->
               e1'
-          | Sil.Const (Sil.Cint _), _ ->
+          | Sil.Const (Const.Cint _), _ ->
               e2'
-          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
+          | _, Sil.Const (Const.Cint i) when IntLit.iszero i ->
               e2'
-          | _, Sil.Const (Sil.Cint _) ->
+          | _, Sil.Const (Const.Cint _) ->
               e1'
           | _ ->
               Sil.BinOp (Sil.LAnd, e1', e2')
@@ -575,13 +575,13 @@ let sym_eval abs e =
         let e2' = eval e2 in
         begin
           match e1', e2' with
-          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
+          | Sil.Const (Const.Cint i), _ when IntLit.iszero i ->
               e2'
-          | Sil.Const (Sil.Cint _), _ ->
+          | Sil.Const (Const.Cint _), _ ->
               e1'
-          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
+          | _, Sil.Const (Const.Cint i) when IntLit.iszero i ->
               e1'
-          | _, Sil.Const (Sil.Cint _) ->
+          | _, Sil.Const (Const.Cint _) ->
               e2'
           | _ ->
               Sil.BinOp (Sil.LOr, e1', e2')
@@ -601,12 +601,14 @@ let sym_eval abs e =
         let isPlusA = oplus = Sil.PlusA in
         let ominus = if isPlusA then Sil.MinusA else Sil.MinusPI in
         let (+++) x y = match x, y with
-          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i -> x
-          | Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (IntLit.add i j))
+          | _, Sil.Const (Const.Cint i) when IntLit.iszero i -> x
+          | Sil.Const (Const.Cint i), Sil.Const (Const.Cint j) ->
+              Sil.Const (Const.Cint (IntLit.add i j))
           | _ -> Sil.BinOp (oplus, x, y) in
         let (---) x y = match x, y with
-          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i -> x
-          | Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (IntLit.sub i j))
+          | _, Sil.Const (Const.Cint i) when IntLit.iszero i -> x
+          | Sil.Const (Const.Cint i), Sil.Const (Const.Cint j) ->
+              Sil.Const (Const.Cint (IntLit.sub i j))
           | _ -> Sil.BinOp (ominus, x, y) in
         (* test if the extensible array at the end of [typ] has elements of type [elt] *)
         let extensible_array_element_typ_equal elt typ =
@@ -623,20 +625,20 @@ let sym_eval abs e =
               e2'
           | _, Sil.Const c when iszero_int_float c ->
               e1'
-          | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
+          | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) ->
               Sil.exp_int (n ++ m)
-          | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
+          | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) ->
               Sil.exp_float (v +. w)
           | Sil.UnOp(Sil.Neg, f1, _), f2
           | f2, Sil.UnOp(Sil.Neg, f1, _) ->
               Sil.BinOp (ominus, f2, f1)
-          | Sil.BinOp (Sil.PlusA, e, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2)
-          | Sil.BinOp (Sil.PlusPI, e, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2)
-          | Sil.Const (Sil.Cint n2), Sil.BinOp (Sil.PlusA, e, Sil.Const (Sil.Cint n1))
-          | Sil.Const (Sil.Cint n2), Sil.BinOp (Sil.PlusPI, e, Sil.Const (Sil.Cint n1)) ->
+          | Sil.BinOp (Sil.PlusA, e, Sil.Const (Const.Cint n1)), Sil.Const (Const.Cint n2)
+          | Sil.BinOp (Sil.PlusPI, e, Sil.Const (Const.Cint n1)), Sil.Const (Const.Cint n2)
+          | Sil.Const (Const.Cint n2), Sil.BinOp (Sil.PlusA, e, Sil.Const (Const.Cint n1))
+          | Sil.Const (Const.Cint n2), Sil.BinOp (Sil.PlusPI, e, Sil.Const (Const.Cint n1)) ->
               e +++ (Sil.exp_int (n1 ++ n2))
-          | Sil.BinOp (Sil.MinusA, Sil.Const (Sil.Cint n1), e), Sil.Const (Sil.Cint n2)
-          | Sil.Const (Sil.Cint n2), Sil.BinOp (Sil.MinusA, Sil.Const (Sil.Cint n1), e) ->
+          | Sil.BinOp (Sil.MinusA, Sil.Const (Const.Cint n1), e), Sil.Const (Const.Cint n2)
+          | Sil.Const (Const.Cint n2), Sil.BinOp (Sil.MinusA, Sil.Const (Const.Cint n1), e) ->
               Sil.exp_int (n1 ++ n2) --- e
           | Sil.BinOp (Sil.MinusA, e1, e2), e3 -> (* (e1-e2)+e3 --> e1 + (e3-e2) *)
               (* progress: brings + to the outside *)
@@ -667,13 +669,13 @@ let sym_eval abs e =
               eval (Sil.UnOp(Sil.Neg, e2', None))
           | _, Sil.Const c when iszero_int_float c ->
               e1'
-          | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
+          | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) ->
               Sil.exp_int (n -- m)
-          | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
+          | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) ->
               Sil.exp_float (v -. w)
           | _, Sil.UnOp (Sil.Neg, f2, _) ->
               eval (e1 +++ f2)
-          | _ , Sil.Const(Sil.Cint n) ->
+          | _ , Sil.Const(Const.Cint n) ->
               eval (e1' +++ (Sil.exp_int (IntLit.neg n)))
           | Sil.Const _, _ ->
               e1' --- e2'
@@ -702,9 +704,9 @@ let sym_eval abs e =
               e1'
           | _, Sil.Const c when isminusone_int_float c ->
               eval (Sil.UnOp (Sil.Neg, e1', None))
-          | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
+          | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) ->
               Sil.exp_int (IntLit.mul n m)
-          | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
+          | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) ->
               Sil.exp_float (v *. w)
           | Sil.Var _, Sil.Var _ ->
               Sil.BinOp(Sil.Mult, e1', e2')
@@ -725,9 +727,9 @@ let sym_eval abs e =
               e1'
           | _, Sil.Const c when isone_int_float c ->
               e1'
-          | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
+          | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) ->
               Sil.exp_int (IntLit.div n m)
-          | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
+          | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) ->
               Sil.exp_float (v /.w)
           | Sil.Sizeof (Typ.Tarray (elt, _), Some len, _), Sil.Sizeof (elt2, None, _)
             (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
@@ -736,7 +738,7 @@ let sym_eval abs e =
           | Sil.Sizeof (Typ.Tarray (elt, Some len), None, _), Sil.Sizeof (elt2, None, _)
             (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
             when Typ.equal elt elt2 ->
-              Sil.Const (Sil.Cint len)
+              Sil.Const (Const.Cint len)
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.Div, e1', e2')
         end
@@ -745,13 +747,13 @@ let sym_eval abs e =
         let e2' = eval e2 in
         begin
           match e1', e2' with
-          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
+          | _, Sil.Const (Const.Cint i) when IntLit.iszero i ->
               Sil.exp_get_undefined false
-          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
+          | Sil.Const (Const.Cint i), _ when IntLit.iszero i ->
               e1'
-          | _, Sil.Const (Sil.Cint i) when IntLit.isone i ->
+          | _, Sil.Const (Const.Cint i) when IntLit.isone i ->
               Sil.exp_zero
-          | Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
+          | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) ->
               Sil.exp_int (IntLit.rem n m)
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.Mod, e1', e2')
@@ -764,11 +766,11 @@ let sym_eval abs e =
         let e1' = eval e1 in
         let e2' = eval e2 in
         begin match e1', e2' with
-          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
+          | Sil.Const (Const.Cint i), _ when IntLit.iszero i ->
               e1'
-          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
+          | _, Sil.Const (Const.Cint i) when IntLit.iszero i ->
               e2'
-          | Sil.Const (Sil.Cint i1), Sil.Const(Sil.Cint i2) ->
+          | Sil.Const (Const.Cint i1), Sil.Const(Const.Cint i2) ->
               Sil.exp_int (IntLit.logand i1 i2)
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.BAnd, e1', e2')
@@ -777,11 +779,11 @@ let sym_eval abs e =
         let e1' = eval e1 in
         let e2' = eval e2 in
         begin match e1', e2' with
-          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
+          | Sil.Const (Const.Cint i), _ when IntLit.iszero i ->
               e2'
-          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
+          | _, Sil.Const (Const.Cint i) when IntLit.iszero i ->
               e1'
-          | Sil.Const (Sil.Cint i1), Sil.Const(Sil.Cint i2) ->
+          | Sil.Const (Const.Cint i1), Sil.Const(Const.Cint i2) ->
               Sil.exp_int (IntLit.logor i1 i2)
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.BOr, e1', e2')
@@ -790,11 +792,11 @@ let sym_eval abs e =
         let e1' = eval e1 in
         let e2' = eval e2 in
         begin match e1', e2' with
-          | Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
+          | Sil.Const (Const.Cint i), _ when IntLit.iszero i ->
               e2'
-          | _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
+          | _, Sil.Const (Const.Cint i) when IntLit.iszero i ->
               e1'
-          | Sil.Const (Sil.Cint i1), Sil.Const(Sil.Cint i2) ->
+          | Sil.Const (Const.Cint i1), Sil.Const(Const.Cint i2) ->
               Sil.exp_int (IntLit.logxor i1 i2)
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.BXor, e1', e2')
@@ -804,9 +806,9 @@ let sym_eval abs e =
         let e2' = eval e2 in
         begin
           match e2' with
-          | Sil.Const (Sil.Cptr_to_fld (fn, typ)) ->
+          | Sil.Const (Const.Cptr_to_fld (fn, typ)) ->
               eval (Sil.Lfield(e1', fn, typ))
-          | Sil.Const (Sil.Cint i) when IntLit.iszero i ->
+          | Sil.Const (Const.Cint i) when IntLit.iszero i ->
               Sil.exp_zero (* cause a NULL dereference *)
           | _ -> Sil.BinOp (Sil.PtrFld, e1', e2')
         end
@@ -848,20 +850,20 @@ let exp_normalize_noabs sub exp =
 
 (** Return [true] if the atom is an inequality *)
 let atom_is_inequality = function
-  | Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Sil.Cint i)) when IntLit.isone i -> true
-  | Sil.Aeq (Sil.BinOp (Sil.Lt, _, _), Sil.Const (Sil.Cint i)) when IntLit.isone i -> true
+  | Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Const.Cint i)) when IntLit.isone i -> true
+  | Sil.Aeq (Sil.BinOp (Sil.Lt, _, _), Sil.Const (Const.Cint i)) when IntLit.isone i -> true
   | _ -> false
 
 (** If the atom is [e<=n] return [e,n] *)
 let atom_exp_le_const = function
-  | Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint i))
+  | Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Const.Cint n)), Sil.Const (Const.Cint i))
     when IntLit.isone i ->
       Some (e1, n)
   | _ -> None
 
 (** If the atom is [n<e] return [n,e] *)
 let atom_const_lt_exp = function
-  | Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), e1), Sil.Const (Sil.Cint i))
+  | Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Const.Cint n), e1), Sil.Const (Const.Cint i))
     when IntLit.isone i ->
       Some (n, e1)
   | _ -> None
@@ -869,23 +871,23 @@ let atom_const_lt_exp = function
 (** Turn an inequality expression into an atom *)
 let mk_inequality e =
   match e with
-  | Sil.BinOp (Sil.Le, base, Sil.Const (Sil.Cint n)) ->
+  | Sil.BinOp (Sil.Le, base, Sil.Const (Const.Cint n)) ->
       (* base <= n case *)
       let nbase = exp_normalize_noabs Sil.sub_empty base in
       (match nbase with
-       | Sil.BinOp(Sil.PlusA, base', Sil.Const (Sil.Cint n')) ->
+       | Sil.BinOp(Sil.PlusA, base', Sil.Const (Const.Cint n')) ->
            let new_offset = Sil.exp_int (n -- n') in
            let new_e = Sil.BinOp (Sil.Le, base', new_offset) in
            Sil.Aeq (new_e, Sil.exp_one)
-       | Sil.BinOp(Sil.PlusA, Sil.Const (Sil.Cint n'), base') ->
+       | Sil.BinOp(Sil.PlusA, Sil.Const (Const.Cint n'), base') ->
            let new_offset = Sil.exp_int (n -- n') in
            let new_e = Sil.BinOp (Sil.Le, base', new_offset) in
            Sil.Aeq (new_e, Sil.exp_one)
-       | Sil.BinOp(Sil.MinusA, base', Sil.Const (Sil.Cint n')) ->
+       | Sil.BinOp(Sil.MinusA, base', Sil.Const (Const.Cint n')) ->
            let new_offset = Sil.exp_int (n ++ n') in
            let new_e = Sil.BinOp (Sil.Le, base', new_offset) in
            Sil.Aeq (new_e, Sil.exp_one)
-       | Sil.BinOp(Sil.MinusA, Sil.Const (Sil.Cint n'), base') ->
+       | Sil.BinOp(Sil.MinusA, Sil.Const (Const.Cint n'), base') ->
            let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in
            let new_e = Sil.BinOp (Sil.Lt, new_offset, base') in
            Sil.Aeq (new_e, Sil.exp_one)
@@ -895,23 +897,23 @@ let mk_inequality e =
            let new_e = Sil.BinOp (Sil.Lt, new_offset, new_base) in
            Sil.Aeq (new_e, Sil.exp_one)
        | _ -> Sil.Aeq (e, Sil.exp_one))
-  | Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), base) ->
+  | Sil.BinOp (Sil.Lt, Sil.Const (Const.Cint n), base) ->
       (* n < base case *)
       let nbase = exp_normalize_noabs Sil.sub_empty base in
       (match nbase with
-       | Sil.BinOp(Sil.PlusA, base', Sil.Const (Sil.Cint n')) ->
+       | Sil.BinOp(Sil.PlusA, base', Sil.Const (Const.Cint n')) ->
            let new_offset = Sil.exp_int (n -- n') in
            let new_e = Sil.BinOp (Sil.Lt, new_offset, base') in
            Sil.Aeq (new_e, Sil.exp_one)
-       | Sil.BinOp(Sil.PlusA, Sil.Const (Sil.Cint n'), base') ->
+       | Sil.BinOp(Sil.PlusA, Sil.Const (Const.Cint n'), base') ->
            let new_offset = Sil.exp_int (n -- n') in
            let new_e = Sil.BinOp (Sil.Lt, new_offset, base') in
            Sil.Aeq (new_e, Sil.exp_one)
-       | Sil.BinOp(Sil.MinusA, base', Sil.Const (Sil.Cint n')) ->
+       | Sil.BinOp(Sil.MinusA, base', Sil.Const (Const.Cint n')) ->
            let new_offset = Sil.exp_int (n ++ n') in
            let new_e = Sil.BinOp (Sil.Lt, new_offset, base') in
            Sil.Aeq (new_e, Sil.exp_one)
-       | Sil.BinOp(Sil.MinusA, Sil.Const (Sil.Cint n'), base') ->
+       | Sil.BinOp(Sil.MinusA, Sil.Const (Const.Cint n'), base') ->
            let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in
            let new_e = Sil.BinOp (Sil.Le, base', new_offset) in
            Sil.Aeq (new_e, Sil.exp_one)
@@ -929,7 +931,7 @@ let inequality_normalize a =
       and integer offset *)
   (** representing inequality [sum(pos) - sum(neg) + off <= 0] *)
   let rec exp_to_posnegoff e = match e with
-    | Sil.Const (Sil.Cint n) -> [],[], n
+    | Sil.Const (Const.Cint n) -> [],[], n
     | Sil.BinOp(Sil.PlusA, e1, e2) | Sil.BinOp(Sil.PlusPI, e1, e2) ->
         let pos1, neg1, n1 = exp_to_posnegoff e1 in
         let pos2, neg2, n2 = exp_to_posnegoff e2 in
@@ -971,7 +973,7 @@ let inequality_normalize a =
         let lhs_e = Sil.BinOp(Sil.MinusA, exp_list_to_sum pos, exp_list_to_sum neg) in
         Sil.BinOp(Sil.Le, lhs_e, Sil.exp_int (IntLit.zero -- n)) in
   let ineq = match a with
-    | Sil.Aeq (ineq, Sil.Const (Sil.Cint i)) when IntLit.isone i ->
+    | Sil.Aeq (ineq, Sil.Const (Const.Cint i)) when IntLit.isone i ->
         ineq
     | _ -> assert false in
   match ineq with
@@ -991,15 +993,15 @@ let exp_reorder e1 e2 = if Sil.exp_compare e1 e2 <= 0 then (e1, e2) else (e2, e1
 let atom_normalize sub a0 =
   let a = Sil.atom_sub sub a0 in
   let rec normalize_eq eq = match eq with
-    | Sil.BinOp(Sil.PlusA, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2)
+    | Sil.BinOp(Sil.PlusA, e1, Sil.Const (Const.Cint n1)), Sil.Const (Const.Cint n2)
     (* e1+n1==n2 ---> e1==n2-n1 *)
-    | Sil.BinOp(Sil.PlusPI, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2) ->
+    | Sil.BinOp(Sil.PlusPI, e1, Sil.Const (Const.Cint n1)), Sil.Const (Const.Cint n2) ->
         (e1, Sil.exp_int (n2 -- n1))
-    | Sil.BinOp(Sil.MinusA, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2)
+    | Sil.BinOp(Sil.MinusA, e1, Sil.Const (Const.Cint n1)), Sil.Const (Const.Cint n2)
     (* e1-n1==n2 ---> e1==n1+n2 *)
-    | Sil.BinOp(Sil.MinusPI, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2) ->
+    | Sil.BinOp(Sil.MinusPI, e1, Sil.Const (Const.Cint n1)), Sil.Const (Const.Cint n2) ->
         (e1, Sil.exp_int (n1 ++ n2))
-    | Sil.BinOp(Sil.MinusA, Sil.Const (Sil.Cint n1), e1), Sil.Const (Sil.Cint n2) ->
+    | Sil.BinOp(Sil.MinusA, Sil.Const (Const.Cint n1), e1), Sil.Const (Const.Cint n2) ->
         (* n1-e1 == n2 -> e1==n1-n2 *)
         (e1, Sil.exp_int (n1 -- n2))
     | Sil.Lfield (e1', fld1, _), Sil.Lfield (e2', fld2, _) ->
@@ -1013,8 +1015,8 @@ let atom_normalize sub a0 =
     | _ -> eq in
   let handle_unary_negation e1 e2 =
     match e1, e2 with
-    | Sil.UnOp (Sil.LNot, e1', _), Sil.Const (Sil.Cint i)
-    | Sil.Const (Sil.Cint i), Sil.UnOp (Sil.LNot, e1', _) when IntLit.iszero i ->
+    | Sil.UnOp (Sil.LNot, e1', _), Sil.Const (Const.Cint i)
+    | Sil.Const (Const.Cint i), Sil.UnOp (Sil.LNot, e1', _) when IntLit.iszero i ->
         (e1', Sil.exp_zero, true)
     | _ -> (e1, e2, false) in
   let handle_boolean_operation from_equality e1 e2 =
@@ -1038,9 +1040,9 @@ let atom_normalize sub a0 =
 
 (** Negate an atom *)
 let atom_negate = function
-  | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
+  | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Const.Cint i)) when IntLit.isone i ->
       mk_inequality (Sil.exp_lt e2 e1)
-  | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
+  | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Const.Cint i)) when IntLit.isone i ->
       mk_inequality (Sil.exp_le e2 e1)
   | Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2)
   | Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2)
@@ -1086,7 +1088,7 @@ let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
     if !Config.curr_language = Config.Java && inst = Sil.Ialloc
     then
       match typ with
-      | Typ.Tfloat _ -> Sil.Const (Sil.Cfloat 0.0)
+      | Typ.Tfloat _ -> Sil.Const (Const.Cfloat 0.0)
       | _ -> Sil.exp_zero
     else
       create_fresh_var () in
@@ -1111,7 +1113,7 @@ let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
   | Typ.Tarray (_, len_opt), None ->
       let len = match len_opt with
         | None -> Sil.exp_get_undefined false
-        | Some len -> Sil.Const (Sil.Cint len) in
+        | Some len -> Sil.Const (Const.Cint len) in
       Sil.Earray (len, [], inst)
   | Typ.Tarray _, Some len ->
       Sil.Earray (len, [], inst)
@@ -1209,7 +1211,8 @@ let pi_tighten_ineq pi =
   let ineq_list, nonineq_list = IList.partition atom_is_inequality pi in
   let diseq_list =
     let get_disequality_info acc = function
-      | Sil.Aneq(Sil.Const (Sil.Cint n), e) | Sil.Aneq(e, Sil.Const (Sil.Cint n)) -> (e, n):: acc
+      | Sil.Aneq(Sil.Const (Const.Cint n), e)
+      | Sil.Aneq(e, Sil.Const (Const.Cint n)) -> (e, n) :: acc
       | _ -> acc in
     IList.fold_left get_disequality_info [] nonineq_list in
   let is_neq e n =
@@ -1252,8 +1255,8 @@ let pi_tighten_ineq pi =
   let nonineq_list' =
     IList.filter
       (function
-        | Sil.Aneq(Sil.Const (Sil.Cint n), e)
-        | Sil.Aneq(e, Sil.Const (Sil.Cint n)) ->
+        | Sil.Aneq(Sil.Const (Const.Cint n), e)
+        | Sil.Aneq(e, Sil.Const (Const.Cint n)) ->
             (not (IList.exists
                     (fun (e', n') -> Sil.exp_equal e e' && IntLit.lt n' n)
                     le_list_tightened)) &&
@@ -1266,13 +1269,13 @@ let pi_tighten_ineq pi =
 
 (** remove duplicate atoms and redundant inequalities from a sorted pi *)
 let rec pi_sorted_remove_redundant = function
-  | (Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint i1)) as a1) ::
-    Sil.Aeq(Sil.BinOp (Sil.Le, e2, Sil.Const (Sil.Cint n2)), Sil.Const (Sil.Cint i2)) :: rest
+  | (Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Const.Cint n1)), Sil.Const (Const.Cint i1)) as a1) ::
+    Sil.Aeq(Sil.BinOp (Sil.Le, e2, Sil.Const (Const.Cint n2)), Sil.Const (Const.Cint i2)) :: rest
     when IntLit.isone i1 && IntLit.isone i2 && Sil.exp_equal e1 e2 && IntLit.lt n1 n2 ->
       (* second inequality redundant *)
       pi_sorted_remove_redundant (a1 :: rest)
-  | Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n1), e1), Sil.Const (Sil.Cint i1)) ::
-    (Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n2), e2), Sil.Const (Sil.Cint i2)) as a2) ::
+  | Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Const.Cint n1), e1), Sil.Const (Const.Cint i1)) ::
+    (Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Const.Cint n2), e2), Sil.Const (Const.Cint i2)) as a2) ::
     rest
     when IntLit.isone i1 && IntLit.isone i2 && Sil.exp_equal e1 e2 && IntLit.lt n1 n2 ->
       (* first inequality redundant *)
@@ -1302,27 +1305,27 @@ let pi_normalize sub sigma pi0 =
   let syntactically_different = function
     | Sil.BinOp(op1, e1, Sil.Const(c1)), Sil.BinOp(op2, e2, Sil.Const(c2))
       when Sil.exp_equal e1 e2 ->
-        Sil.binop_equal op1 op2 && Sil.binop_injective op1 && not (Sil.const_equal c1 c2)
+        Sil.binop_equal op1 op2 && Sil.binop_injective op1 && not (Const.equal c1 c2)
     | e1, Sil.BinOp(op2, e2, Sil.Const(c2))
       when Sil.exp_equal e1 e2 ->
         Sil.binop_injective op2 &&
         Sil.binop_is_zero_runit op2 &&
-        not (Sil.const_equal (Sil.Cint IntLit.zero) c2)
+        not (Const.equal (Const.Cint IntLit.zero) c2)
     | Sil.BinOp(op1, e1, Sil.Const(c1)), e2
       when Sil.exp_equal e1 e2 ->
         Sil.binop_injective op1 &&
         Sil.binop_is_zero_runit op1 &&
-        not (Sil.const_equal (Sil.Cint IntLit.zero) c1)
+        not (Const.equal (Const.Cint IntLit.zero) c1)
     | _ -> false in
   let filter_useful_atom =
     let unsigned_exps = lazy (sigma_get_unsigned_exps sigma) in
     function
-    | Sil.Aneq ((Sil.Var _) as e, Sil.Const (Sil.Cint n)) when IntLit.isnegative n ->
+    | Sil.Aneq ((Sil.Var _) as e, Sil.Const (Const.Cint n)) when IntLit.isnegative n ->
         not (IList.exists (Sil.exp_equal e) (Lazy.force unsigned_exps))
     | Sil.Aneq(e1, e2) ->
         not (syntactically_different (e1, e2))
     | Sil.Aeq(Sil.Const c1, Sil.Const c2) ->
-        not (Sil.const_equal c1 c2)
+        not (Const.equal c1 c2)
     | _ -> true in
   let pi' =
     IList.stable_sort
@@ -1670,19 +1673,19 @@ let sigma_intro_nonemptylseg e1 e2 sigma =
 let normalize_and_strengthen_atom (p : normal t) (a : Sil.atom) : Sil.atom =
   let a' = atom_normalize p.sub a in
   match a' with
-  | Sil.Aeq (Sil.BinOp (Sil.Le, Sil.Var id, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint i))
+  | Sil.Aeq (Sil.BinOp (Sil.Le, Sil.Var id, Sil.Const (Const.Cint n)), Sil.Const (Const.Cint i))
     when IntLit.isone i ->
       let lower = Sil.exp_int (n -- IntLit.one) in
       let a_lower = Sil.Aeq (Sil.BinOp (Sil.Lt, lower, Sil.Var id), Sil.exp_one) in
       if not (IList.mem Sil.atom_equal a_lower p.pi) then a'
       else Sil.Aeq (Sil.Var id, Sil.exp_int n)
-  | Sil.Aeq (Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), Sil.Var id), Sil.Const (Sil.Cint i))
+  | Sil.Aeq (Sil.BinOp (Sil.Lt, Sil.Const (Const.Cint n), Sil.Var id), Sil.Const (Const.Cint i))
     when IntLit.isone i ->
       let upper = Sil.exp_int (n ++ IntLit.one) in
       let a_upper = Sil.Aeq (Sil.BinOp (Sil.Le, Sil.Var id, upper), Sil.exp_one) in
       if not (IList.mem Sil.atom_equal a_upper p.pi) then a'
       else Sil.Aeq (Sil.Var id, upper)
-  | Sil.Aeq (Sil.BinOp (Sil.Ne, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
+  | Sil.Aeq (Sil.BinOp (Sil.Ne, e1, e2), Sil.Const (Const.Cint i)) when IntLit.isone i ->
       Sil.Aneq (e1, e2)
   | _ -> a'
 
@@ -2191,7 +2194,7 @@ let compute_reindexing fav_add get_id_offset list =
 
 let compute_reindexing_from_indices indices =
   let get_id_offset = function
-    | Sil.BinOp (Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint offset)) ->
+    | Sil.BinOp (Sil.PlusA, Sil.Var id, Sil.Const(Const.Cint offset)) ->
         if Ident.is_primed id then Some (id, offset) else None
     | _ -> None in
   let fav_add = Sil.exp_fav_add in
@@ -2218,8 +2221,8 @@ let prop_rename_array_indices prop =
     let indices = sigma_get_array_indices prop.sigma in
     let not_same_base_lt_offsets e1 e2 =
       match e1, e2 with
-      | Sil.BinOp(Sil.PlusA, e1', Sil.Const (Sil.Cint n1')),
-        Sil.BinOp(Sil.PlusA, e2', Sil.Const (Sil.Cint n2')) ->
+      | Sil.BinOp(Sil.PlusA, e1', Sil.Const (Const.Cint n1')),
+        Sil.BinOp(Sil.PlusA, e2', Sil.Const (Const.Cint n2')) ->
           not (Sil.exp_equal e1' e2' && IntLit.lt n1' n2')
       | _ -> true in
     let rec select_minimal_indices indices_seen = function
@@ -2830,8 +2833,8 @@ let find_equal_formal_path e prop =
 (** translate an if-then-else expression *)
 let trans_if_then_else ((idl1, stml1), e1) ((idl2, stml2), e2) ((idl3, stml3), e3) loc =
   match sym_eval false e1 with
-  | Sil.Const (Sil.Cint i) when IntLit.iszero i -> (idl1@idl3, stml1@stml3), e3
-  | Sil.Const (Sil.Cint _) -> (idl1@idl2, stml1@stml2), e2
+  | Sil.Const (Const.Cint i) when IntLit.iszero i -> (idl1@idl3, stml1@stml3), e3
+  | Sil.Const (Const.Cint _) -> (idl1@idl2, stml1@stml2), e2
   | _ ->
       let e1not = Sil.UnOp(Sil.LNot, e1, None) in
       let id = Ident.create_fresh Ident.knormal in
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index fd97d7a5e..eba84c034 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -79,7 +79,7 @@ end = struct
 
   let from_leq acc (e1, e2) =
     match e1, e2 with
-    | Sil.BinOp(Sil.MinusA, (Sil.Var id11 as e11), (Sil.Var id12 as e12)), Sil.Const (Sil.Cint n)
+    | Sil.BinOp(Sil.MinusA, (Sil.Var id11 as e11), (Sil.Var id12 as e12)), Sil.Const (Const.Cint n)
       when not (Ident.equal id11 id12) ->
         (match IntLit.to_signed n with
          | None -> acc (* ignore: constraint algorithm only terminates on signed integers *)
@@ -88,7 +88,7 @@ end = struct
     | _ -> acc
   let from_lt acc (e1, e2) =
     match e1, e2 with
-    | Sil.Const (Sil.Cint n), Sil.BinOp(Sil.MinusA, (Sil.Var id21 as e21), (Sil.Var id22 as e22))
+    | Sil.Const (Const.Cint n), Sil.BinOp(Sil.MinusA, (Sil.Var id21 as e21), (Sil.Var id22 as e22))
       when not (Ident.equal id21 id22) ->
         (match IntLit.to_signed n with
          | None -> acc (* ignore: constraint algorithm only terminates on signed integers *)
@@ -264,7 +264,7 @@ end = struct
     let leqs_sorted = IList.sort leq_compare leqs in
     let have_same_key leq1 leq2 =
       match leq1, leq2 with
-      | (e1, Sil.Const (Sil.Cint n1)), (e2, Sil.Const (Sil.Cint n2)) ->
+      | (e1, Sil.Const (Const.Cint n1)), (e2, Sil.Const (Const.Cint n2)) ->
           Sil.exp_equal e1 e2 && IntLit.leq n1 n2
       | _, _ -> false in
     remove_redundancy have_same_key [] leqs_sorted
@@ -272,7 +272,7 @@ end = struct
     let lts_sorted = IList.sort lt_compare lts in
     let have_same_key lt1 lt2 =
       match lt1, lt2 with
-      | (Sil.Const (Sil.Cint n1), e1), (Sil.Const (Sil.Cint n2), e2) ->
+      | (Sil.Const (Const.Cint n1), e1), (Sil.Const (Const.Cint n2), e2) ->
           Sil.exp_equal e1 e2 && IntLit.geq n1 n2
       | _, _ -> false in
     remove_redundancy have_same_key [] lts_sorted
@@ -298,13 +298,13 @@ end = struct
         with Not_found -> Sil.ExpMap.add e new_lower lmap in
       let rec umap_create_from_leqs umap = function
         | [] -> umap
-        | (e1, Sil.Const (Sil.Cint upper1)):: leqs_rest ->
+        | (e1, Sil.Const (Const.Cint upper1)):: leqs_rest ->
             let umap' = umap_add umap e1 upper1 in
             umap_create_from_leqs umap' leqs_rest
         | _:: leqs_rest -> umap_create_from_leqs umap leqs_rest in
       let rec lmap_create_from_lts lmap = function
         | [] -> lmap
-        | (Sil.Const (Sil.Cint lower1), e1):: lts_rest ->
+        | (Sil.Const (Const.Cint lower1), e1):: lts_rest ->
             let lmap' = lmap_add lmap e1 lower1 in
             lmap_create_from_lts lmap' lts_rest
         | _:: lts_rest -> lmap_create_from_lts lmap lts_rest in
@@ -357,10 +357,10 @@ end = struct
     let process_atom = function
       | Sil.Aneq (e1, e2) -> (* != *)
           neqs := (e1, e2) :: !neqs
-      | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i -> (* <= *)
-          leqs := (e1, e2) :: !leqs
-      | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i -> (* < *)
-          lts := (e1, e2) :: !lts
+      | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Const.Cint i)) when IntLit.isone i ->
+          leqs := (e1, e2) :: !leqs (* <= *)
+      | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Const.Cint i)) when IntLit.isone i ->
+          lts := (e1, e2) :: !lts (* < *)
       | Sil.Aeq _ -> () in
     IList.iter process_atom pi;
     saturate { leqs = !leqs; lts = !lts; neqs = !neqs }
@@ -414,19 +414,19 @@ end = struct
   let check_le { leqs = leqs; lts = lts; neqs = _ } e1 e2 =
     (* L.d_str "check_le "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
     match e1, e2 with
-    | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> IntLit.leq n1 n2
+    | Sil.Const (Const.Cint n1), Sil.Const (Const.Cint n2) -> IntLit.leq n1 n2
     | Sil.BinOp (Sil.MinusA, Sil.Sizeof (t1, None, _), Sil.Sizeof (t2, None, _)),
-      Sil.Const(Sil.Cint n2)
+      Sil.Const(Const.Cint n2)
       when IntLit.isminusone n2 && type_size_comparable t1 t2 ->
         (* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
         check_type_size_lt t1 t2
-    | e, Sil.Const (Sil.Cint n) -> (* [e <= n' <= n |- e <= n] *)
+    | e, Sil.Const (Const.Cint n) -> (* [e <= n' <= n |- e <= n] *)
         IList.exists (function
-            | e', Sil.Const (Sil.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' n
+            | e', Sil.Const (Const.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' n
             | _, _ -> false) leqs
-    | Sil.Const (Sil.Cint n), e -> (* [ n-1 <= n' < e |- n <= e] *)
+    | Sil.Const (Const.Cint n), e -> (* [ n-1 <= n' < e |- n <= e] *)
         IList.exists (function
-            | Sil.Const (Sil.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq (n -- IntLit.one) n'
+            | Sil.Const (Const.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq (n -- IntLit.one) n'
             | _, _ -> false) lts
     | _ -> Sil.exp_equal e1 e2
 
@@ -434,14 +434,14 @@ end = struct
   let check_lt { leqs = leqs; lts = lts; neqs = _ } e1 e2 =
     (* L.d_str "check_lt "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
     match e1, e2 with
-    | Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> IntLit.lt n1 n2
-    | Sil.Const (Sil.Cint n), e -> (* [n <= n' < e  |- n < e] *)
+    | Sil.Const (Const.Cint n1), Sil.Const (Const.Cint n2) -> IntLit.lt n1 n2
+    | Sil.Const (Const.Cint n), e -> (* [n <= n' < e  |- n < e] *)
         IList.exists (function
-            | Sil.Const (Sil.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq n n'
+            | Sil.Const (Const.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq n n'
             | _, _ -> false) lts
-    | e, Sil.Const (Sil.Cint n) -> (* [e <= n' <= n-1 |- e < n] *)
+    | e, Sil.Const (Const.Cint n) -> (* [e <= n' <= n-1 |- e < n] *)
         IList.exists (function
-            | e', Sil.Const (Sil.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' (n -- IntLit.one)
+            | e', Sil.Const (Const.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' (n -- IntLit.one)
             | _, _ -> false) leqs
     | _ -> false
 
@@ -453,15 +453,15 @@ end = struct
   (** Find a IntLit.t n such that [t |- e<=n] if possible. *)
   let compute_upper_bound { leqs = leqs; lts = _; neqs = _ } e1 =
     match e1 with
-    | Sil.Const (Sil.Cint n1) -> Some n1
+    | Sil.Const (Const.Cint n1) -> Some n1
     | _ ->
         let e_upper_list =
           IList.filter (function
-              | e', Sil.Const (Sil.Cint _) -> Sil.exp_equal e1 e'
+              | e', Sil.Const (Const.Cint _) -> Sil.exp_equal e1 e'
               | _, _ -> false) leqs in
         let upper_list =
           IList.map (function
-              | _, Sil.Const (Sil.Cint n) -> n
+              | _, Sil.Const (Const.Cint n) -> n
               | _ -> assert false) e_upper_list in
         if upper_list == [] then None
         else Some (compute_min_from_nonempty_int_list upper_list)
@@ -469,16 +469,16 @@ end = struct
   (** Find a IntLit.t n such that [t |- n < e] if possible. *)
   let compute_lower_bound { leqs = _; lts = lts; neqs = _ } e1 =
     match e1 with
-    | Sil.Const (Sil.Cint n1) -> Some (n1 -- IntLit.one)
+    | Sil.Const (Const.Cint n1) -> Some (n1 -- IntLit.one)
     | Sil.Sizeof _ -> Some IntLit.zero
     | _ ->
         let e_lower_list =
           IList.filter (function
-              | Sil.Const (Sil.Cint _), e' -> Sil.exp_equal e1 e'
+              | Sil.Const (Const.Cint _), e' -> Sil.exp_equal e1 e'
               | _, _ -> false) lts in
         let lower_list =
           IList.map (function
-              | Sil.Const (Sil.Cint n), _ -> n
+              | Sil.Const (Const.Cint n), _ -> n
               | _ -> assert false) e_lower_list in
         if lower_list == [] then None
         else Some (compute_max_from_nonempty_int_list lower_list)
@@ -524,14 +524,14 @@ let check_equal prop e1 e2 =
     Sil.exp_equal n_e1 n_e2 in
   let check_equal_const () =
     match n_e1, n_e2 with
-    | Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)), e2
-    | e2, Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)) ->
+    | Sil.BinOp (Sil.PlusA, e1, Sil.Const (Const.Cint d)), e2
+    | e2, Sil.BinOp (Sil.PlusA, e1, Sil.Const (Const.Cint d)) ->
         if Sil.exp_equal e1 e2 then IntLit.iszero d
         else false
-    | Sil.Const c1, Sil.Lindex(Sil.Const c2, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
-        Sil.const_equal c1 c2
-    | Sil.Lindex(Sil.Const c1, Sil.Const (Sil.Cint i)), Sil.Const c2 when IntLit.iszero i ->
-        Sil.const_equal c1 c2
+    | Sil.Const c1, Sil.Lindex(Sil.Const c2, Sil.Const (Const.Cint i)) when IntLit.iszero i ->
+        Const.equal c1 c2
+    | Sil.Lindex(Sil.Const c1, Sil.Const (Const.Cint i)), Sil.Const c2 when IntLit.iszero i ->
+        Const.equal c1 c2
     | _, _ -> false in
   let check_equal_pi () =
     let eq = Sil.Aeq(n_e1, n_e2) in
@@ -565,9 +565,9 @@ let is_root prop base_exp exp =
 let get_bounds prop _e =
   let e_norm = Prop.exp_normalize_prop prop _e in
   let e_root, off = match e_norm with
-    | Sil.BinOp (Sil.PlusA, e, Sil.Const (Sil.Cint n1)) ->
+    | Sil.BinOp (Sil.PlusA, e, Sil.Const (Const.Cint n1)) ->
         e, IntLit.neg n1
-    | Sil.BinOp (Sil.MinusA, e, Sil.Const (Sil.Cint n1)) ->
+    | Sil.BinOp (Sil.MinusA, e, Sil.Const (Const.Cint n1)) ->
         e, n1
     | _ ->
         e_norm, IntLit.zero in
@@ -587,22 +587,23 @@ let check_disequal prop e1 e2 =
   let check_disequal_const () =
     match n_e1, n_e2 with
     | Sil.Const c1, Sil.Const c2 ->
-        (Sil.const_kind_equal c1 c2) && not (Sil.const_equal c1 c2)
-    | Sil.Const c1, Sil.Lindex(Sil.Const c2, Sil.Const (Sil.Cint d)) ->
+        (Const.kind_equal c1 c2) && not (Const.equal c1 c2)
+    | Sil.Const c1, Sil.Lindex(Sil.Const c2, Sil.Const (Const.Cint d)) ->
         if IntLit.iszero d
-        then not (Sil.const_equal c1 c2) (* offset=0 is no offset *)
-        else Sil.const_equal c1 c2 (* same base, different offsets *)
-    | Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d1)), Sil.BinOp (Sil.PlusA, e2, Sil.Const (Sil.Cint d2)) ->
+        then not (Const.equal c1 c2) (* offset=0 is no offset *)
+        else Const.equal c1 c2 (* same base, different offsets *)
+    | Sil.BinOp (Sil.PlusA, e1, Sil.Const (Const.Cint d1)),
+      Sil.BinOp (Sil.PlusA, e2, Sil.Const (Const.Cint d2)) ->
         if Sil.exp_equal e1 e2 then IntLit.neq d1 d2
         else false
-    | Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)), e2
-    | e2, Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)) ->
+    | Sil.BinOp (Sil.PlusA, e1, Sil.Const (Const.Cint d)), e2
+    | e2, Sil.BinOp (Sil.PlusA, e1, Sil.Const (Const.Cint d)) ->
         if Sil.exp_equal e1 e2 then not (IntLit.iszero d)
         else false
-    | Sil.Lindex(Sil.Const c1, Sil.Const (Sil.Cint d)), Sil.Const c2 ->
-        if IntLit.iszero d then not (Sil.const_equal c1 c2) else Sil.const_equal c1 c2
+    | Sil.Lindex(Sil.Const c1, Sil.Const (Const.Cint d)), Sil.Const c2 ->
+        if IntLit.iszero d then not (Const.equal c1 c2) else Const.equal c1 c2
     | Sil.Lindex(Sil.Const c1, Sil.Const d1), Sil.Lindex (Sil.Const c2, Sil.Const d2) ->
-        Sil.const_equal c1 c2 && not (Sil.const_equal d1 d2)
+        Const.equal c1 c2 && not (Const.equal d1 d2)
     | _, _ -> false in
   let ineq = lazy (Inequalities.from_prop prop) in
   let check_pi_implies_disequal e1 e2 =
@@ -674,7 +675,7 @@ let check_disequal prop e1 e2 =
 let check_le_normalized prop e1 e2 =
   (* L.d_str "check_le_normalized "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
   let eL, eR, off = match e1, e2 with
-    | Sil.BinOp(Sil.MinusA, f1, f2), Sil.Const (Sil.Cint n) ->
+    | Sil.BinOp(Sil.MinusA, f1, f2), Sil.Const (Const.Cint n) ->
         if Sil.exp_equal f1 f2
         then Sil.exp_zero, Sil.exp_zero, n
         else f1, f2, n
@@ -731,9 +732,9 @@ let check_atom prop a0 =
     close_out outc;
   end;
   match a with
-  | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i))
+  | Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Const.Cint i))
     when IntLit.isone i -> check_le_normalized prop e1 e2
-  | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i))
+  | Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Const.Cint i))
     when IntLit.isone i -> check_lt_normalized prop e1 e2
   | Sil.Aeq (e1, e2) -> check_equal prop e1 e2
   | Sil.Aneq (e1, e2) -> check_disequal prop e1 e2
@@ -777,7 +778,7 @@ let check_inconsistency_two_hpreds prop =
     | (Sil.Hdllseg (Sil.Lseg_NE, _, iF, _, _, iB, _) as hpred) :: sigma_rest ->
         if Sil.exp_equal iF e || Sil.exp_equal iB e then true
         else f e (hpred:: sigma_seen) sigma_rest
-    | Sil.Hlseg (Sil.Lseg_PE, _, e1, Sil.Const (Sil.Cint i), _) as hpred :: sigma_rest
+    | Sil.Hlseg (Sil.Lseg_PE, _, e1, Sil.Const (Const.Cint i), _) as hpred :: sigma_rest
       when IntLit.iszero i ->
         if Sil.exp_equal e1 e then true
         else f e (hpred:: sigma_seen) sigma_rest
@@ -790,7 +791,7 @@ let check_inconsistency_two_hpreds prop =
           let e_new = Prop.exp_normalize_prop prop_new e
           in f e_new [] sigma_new
         else f e (hpred:: sigma_seen) sigma_rest
-    | Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, Sil.Const (Sil.Cint i), _, _) as hpred :: sigma_rest
+    | Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, Sil.Const (Const.Cint i), _, _) as hpred :: sigma_rest
       when IntLit.iszero i ->
         if Sil.exp_equal e1 e then true
         else f e (hpred:: sigma_seen) sigma_rest
@@ -848,11 +849,11 @@ let check_inconsistency_base prop =
   let inconsistent_atom = function
     | Sil.Aeq (e1, e2) ->
         (match e1, e2 with
-         | Sil.Const c1, Sil.Const c2 -> not (Sil.const_equal c1 c2)
+         | Sil.Const c1, Sil.Const c2 -> not (Const.equal c1 c2)
          | _ -> check_disequal prop e1 e2)
     | Sil.Aneq (e1, e2) ->
         (match e1, e2 with
-         | Sil.Const c1, Sil.Const c2 -> Sil.const_equal c1 c2
+         | Sil.Const c1, Sil.Const c2 -> Const.equal c1 c2
          | _ -> (Sil.exp_compare e1 e2 = 0)) in
   let inconsistent_inequalities () =
     let ineq = Inequalities.from_prop prop in
@@ -1161,11 +1162,11 @@ let exp_imply calc_missing subs e1_in e2_in : subst2 =
         if Pvar.equal v1 v2 then subs
         else raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2))))
     | Sil.Const c1, Sil.Const c2 ->
-        if (Sil.const_equal c1 c2) then subs
+        if (Const.equal c1 c2) then subs
         else raise (IMPL_EXC ("constants not equal", subs, (EXC_FALSE_EXPS (e1, e2))))
-    | Sil.Const (Sil.Cint _), Sil.BinOp (Sil.PlusPI, _, _) ->
+    | Sil.Const (Const.Cint _), Sil.BinOp (Sil.PlusPI, _, _) ->
         raise (IMPL_EXC ("pointer+index cannot evaluate to a constant", subs, (EXC_FALSE_EXPS (e1, e2))))
-    | Sil.Const (Sil.Cint n1), Sil.BinOp (Sil.PlusA, f1, Sil.Const (Sil.Cint n2)) ->
+    | Sil.Const (Const.Cint n1), Sil.BinOp (Sil.PlusA, f1, Sil.Const (Const.Cint n2)) ->
         do_imply subs (Sil.exp_int (n1 -- n2)) f1
     | Sil.BinOp(op1, e1, f1), Sil.BinOp(op2, e2, f2) when op1 == op2 ->
         do_imply (do_imply subs e1 e2) f1 f2
@@ -1203,9 +1204,9 @@ let path_to_id path =
          | Some s -> Some (s ^ "_" ^ (Sil.exp_to_string ind)))
     | Sil.Lvar _ ->
         Some (Sil.exp_to_string path)
-    | Sil.Const (Sil.Cstr s) ->
+    | Sil.Const (Const.Cstr s) ->
         Some ("_const_str_" ^ s)
-    | Sil.Const (Sil.Cclass c) ->
+    | Sil.Const (Const.Cclass c) ->
         Some ("_const_class_" ^ Ident.name_to_string c)
     | Sil.Const _ -> None
     | _ ->
@@ -1945,13 +1946,13 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
     | Sil.Hpointsto (_e2, _, _) ->
         let e2 = Sil.exp_sub (snd subs) _e2 in
         (match e2 with
-         | Sil.Const (Sil.Cstr s) -> Some (s, true)
-         | Sil.Const (Sil.Cclass c) -> Some (Ident.name_to_string c, false)
+         | Sil.Const (Const.Cstr s) -> Some (s, true)
+         | Sil.Const (Const.Cclass c) -> Some (Ident.name_to_string c, false)
          | _ -> None)
     | _ -> None in
   let mk_constant_string_hpred s = (* create an hpred from a constant string *)
     let len = IntLit.of_int (1 + String.length s) in
-    let root = Sil.Const (Sil.Cstr s) in
+    let root = Sil.Const (Const.Cstr s) in
     let sexp =
       let index = Sil.exp_int (IntLit.of_int (String.length s)) in
       match !Config.curr_language with
@@ -1978,9 +1979,11 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
           Sil.Sizeof (Typ.Tstruct typ, None, Sil.Subtype.exact) in
     Sil.Hpointsto (root, sexp, const_string_texp) in
   let mk_constant_class_hpred s = (* creat an hpred from a constant class *)
-    let root = Sil.Const (Sil.Cclass (Ident.string_to_name s)) in
+    let root = Sil.Const (Const.Cclass (Ident.string_to_name s)) in
     let sexp = (* TODO: add appropriate fields *)
-      Sil.Estruct ([(Ident.create_fieldname (Mangled.from_string "java.lang.Class.name") 0, Sil.Eexp ((Sil.Const (Sil.Cstr s), Sil.Inone)))], Sil.inst_none) in
+      Sil.Estruct
+        ([(Ident.create_fieldname (Mangled.from_string "java.lang.Class.name") 0,
+           Sil.Eexp ((Sil.Const (Const.Cstr s), Sil.Inone)))], Sil.inst_none) in
     let class_texp =
       let class_type =
         Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.Class") in
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index 491d5fbf9..66f13758a 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -51,7 +51,7 @@ let check_bad_index pname p len index loc =
     | Some _, Some _ -> true
     | _ -> false in
   let get_const_opt = function
-    | Sil.Const (Sil.Cint n) -> Some n
+    | Sil.Const (Const.Cint n) -> Some n
     | _ -> None in
   if not (index_provably_in_bound ()) then
     begin
@@ -129,7 +129,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
     | Typ.Tarray (t', len_), off ->
         let len = match len_ with
           | None -> Sil.Var (new_id ())
-          | Some len -> Sil.Const (Sil.Cint len) in
+          | Some len -> Sil.Const (Const.Cint len) in
         (match off with
          | [] ->
              ([], Sil.Earray (len, [], inst), t)
@@ -303,7 +303,7 @@ and array_case_analysis_index pname tenv orig_prop
     IList.exists (fun (i, _) -> Prover.check_equal Prop.prop_emp index i) array_cont in
   let array_is_full =
     match array_len with
-    | Sil.Const (Sil.Cint n') -> IntLit.geq (IntLit.of_int (IList.length array_cont)) n'
+    | Sil.Const (Const.Cint n') -> IntLit.geq (IntLit.of_int (IList.length array_cont)) n'
     | _ -> false in
 
   if index_in_array then
@@ -441,7 +441,7 @@ let mk_ptsto_exp_footprint
   let create_ptsto footprint_part off0 = match root, off0, typ with
     | Sil.Lvar pvar, [], Typ.Tfun _ ->
         let fun_name = Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in
-        let fun_exp = Sil.Const (Sil.Cfun fun_name) in
+        let fun_exp = Sil.Const (Const.Cfun fun_name) in
         ([], Prop.mk_ptsto root (Sil.Eexp (fun_exp, inst)) (Sil.Sizeof (typ, None, st)))
     | _, [], Typ.Tfun _ ->
         let atoms, se, t =
diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml
index fc2bfaaa0..db9e2a489 100644
--- a/infer/src/backend/state.ml
+++ b/infer/src/backend/state.ml
@@ -15,7 +15,7 @@ open! Utils
 module L = Logging
 module F = Format
 
-type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option
+type const_map = Cfg.Node.t -> Sil.exp -> Const.t option
 
 (** failure statistics for symbolic execution on a given node *)
 type failure_stats = {
diff --git a/infer/src/backend/state.mli b/infer/src/backend/state.mli
index 705aba8ce..13e340d75 100644
--- a/infer/src/backend/state.mli
+++ b/infer/src/backend/state.mli
@@ -18,7 +18,7 @@ type t
 (** Add diverging states *)
 val add_diverging_states : Paths.PathSet.t -> unit
 
-type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option
+type const_map = Cfg.Node.t -> Sil.exp -> Const.t option
 
 (** Get the constant map for the current procedure. *)
 val get_const_map : unit -> const_map
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 00f9fd332..fe0beec6a 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -35,7 +35,7 @@ let rec unroll_type tenv typ off =
       end
   | Typ.Tarray (typ', _), Sil.Off_index _ ->
       typ'
-  | _, Sil.Off_index (Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
+  | _, Sil.Off_index (Sil.Const (Const.Cint i)) when IntLit.iszero i ->
       typ
   | _ ->
       L.d_strln ".... Invalid Field Access ....";
@@ -316,9 +316,9 @@ let rec prune ~positive condition prop =
   match condition with
   | Sil.Var _ | Sil.Lvar _ ->
       prune_ne ~positive condition Sil.exp_zero prop
-  | Sil.Const (Sil.Cint i) when IntLit.iszero i ->
+  | Sil.Const (Const.Cint i) when IntLit.iszero i ->
       if positive then Propset.empty else Propset.singleton prop
-  | Sil.Const (Sil.Cint _) | Sil.Sizeof _ | Sil.Const (Sil.Cstr _) | Sil.Const (Sil.Cclass _) ->
+  | Sil.Const (Const.Cint _ | Const.Cstr _ | Const.Cclass _) | Sil.Sizeof _ ->
       if positive then Propset.singleton prop else Propset.empty
   | Sil.Const _ ->
       assert false
@@ -328,13 +328,13 @@ let rec prune ~positive condition prop =
       prune ~positive:(not positive) condition' prop
   | Sil.UnOp _ ->
       assert false
-  | Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i))
-  | Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e) when IntLit.iszero i && not (IntLit.isnull i) ->
+  | Sil.BinOp (Sil.Eq, e, Sil.Const (Const.Cint i))
+  | Sil.BinOp (Sil.Eq, Sil.Const (Const.Cint i), e) when IntLit.iszero i && not (IntLit.isnull i) ->
       prune ~positive:(not positive) e prop
   | Sil.BinOp (Sil.Eq, e1, e2) ->
       prune_ne ~positive:(not positive) e1 e2 prop
-  | Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i))
-  | Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e) when IntLit.iszero i && not (IntLit.isnull i) ->
+  | Sil.BinOp (Sil.Ne, e, Sil.Const (Const.Cint i))
+  | Sil.BinOp (Sil.Ne, Sil.Const (Const.Cint i), e) when IntLit.iszero i && not (IntLit.isnull i) ->
       prune ~positive e prop
   | Sil.BinOp (Sil.Ne, e1, e2) ->
       prune_ne ~positive e1 e2 prop
@@ -403,16 +403,16 @@ let check_constant_string_dereference lexp =
     let c = try Char.code (String.get s (IntLit.to_int n)) with Invalid_argument _ -> 0 in
     Sil.exp_int (IntLit.of_int c) in
   match lexp with
-  | Sil.BinOp(Sil.PlusPI, Sil.Const (Sil.Cstr s), e)
-  | Sil.Lindex (Sil.Const (Sil.Cstr s), e) ->
+  | Sil.BinOp(Sil.PlusPI, Sil.Const (Const.Cstr s), e)
+  | Sil.Lindex (Sil.Const (Const.Cstr s), e) ->
       let value = match e with
-        | Sil.Const (Sil.Cint n)
+        | Sil.Const (Const.Cint n)
           when IntLit.geq n IntLit.zero &&
                IntLit.leq n (IntLit.of_int (String.length s)) ->
             string_lookup s n
         | _ -> Sil.exp_get_undefined false in
       Some value
-  | Sil.Const (Sil.Cstr s) ->
+  | Sil.Const (Const.Cstr s) ->
       Some (string_lookup s IntLit.zero)
   | _ -> None
 
@@ -447,8 +447,8 @@ let check_already_dereferenced pname cond prop =
         Some id
     | Sil.UnOp(Sil.LNot, e, _) ->
         is_check_zero e
-    | Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Const Sil.Cint i, Sil.Var id)
-    | Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Var id, Sil.Const Sil.Cint i) when IntLit.iszero i ->
+    | Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Const Const.Cint i, Sil.Var id)
+    | Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Var id, Sil.Const Const.Cint i) when IntLit.iszero i ->
         Some id
     | _ -> None in
   let dereferenced_line = match is_check_zero cond with
@@ -480,7 +480,7 @@ let check_deallocate_static_memory prop_after =
       when Pvar.is_local pv || Pvar.is_global pv ->
         let freed_desc = Errdesc.explain_deallocate_stack_var pv ra in
         raise (Exceptions.Deallocate_stack_variable freed_desc)
-    | Sil.Const (Sil.Cstr s), Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra) ->
+    | Sil.Const (Const.Cstr s), Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra) ->
         let freed_desc = Errdesc.explain_deallocate_constant_string s ra in
         raise (Exceptions.Deallocate_static_memory freed_desc)
     | _ -> () in
@@ -693,7 +693,7 @@ let call_constructor_url_update_args pname actual_params =
          [(Some "java.lang"), "String"] Procname.Non_Static) in
   if (Procname.equal url_pname pname) then
     (match actual_params with
-     | [this; (Sil.Const (Sil.Cstr s), atype)] ->
+     | [this; (Sil.Const (Const.Cstr s), atype)] ->
          let parts = Str.split (Str.regexp_string "://") s in
          (match parts with
           | frst:: _ ->
@@ -703,10 +703,10 @@ let call_constructor_url_update_args pname actual_params =
                  frst = "mailto" ||
                  frst = "jar"
               then
-                [this; (Sil.Const (Sil.Cstr frst), atype)]
+                [this; (Sil.Const (Const.Cstr frst), atype)]
               else actual_params
           | _ -> actual_params)
-     | [this; _, atype] -> [this; (Sil.Const (Sil.Cstr "file"), atype)]
+     | [this; _, atype] -> [this; (Sil.Const (Const.Cstr "file"), atype)]
      | _ -> actual_params)
   else actual_params
 
@@ -1006,7 +1006,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
         let exp' = Prop.exp_normalize_prop prop_ exp in
         let instr' = match exp' with
           | Sil.Closure c ->
-              let proc_exp = Sil.Const (Sil.Cfun c.name) in
+              let proc_exp = Sil.Const (Const.Cfun c.name) in
               let proc_exp' = Prop.exp_normalize_prop prop_ proc_exp in
               let par' = IList.map (fun (id_exp, _, typ) -> (id_exp, typ)) c.captured_vars in
               Sil.Call (ret, proc_exp', par' @ par, loc, call_flags)
@@ -1062,7 +1062,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
               !Config.curr_language = Config.Clang && Sil.exp_is_zero exp
           | _ -> false in
         match Prop.exp_normalize_prop Prop.prop_emp cond with
-        | Sil.Const (Sil.Cint i) when report_condition_always_true_false i ->
+        | Sil.Const (Const.Cint i) when report_condition_always_true_false i ->
             let node = State.get_node () in
             let desc = Errdesc.explain_condition_always_true_false i cond node loc in
             let exn =
@@ -1095,12 +1095,12 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       check_condition_always_true_false ();
       let n_cond, prop = check_arith_norm_exp current_pname cond prop__ in
       ret_old_path (Propset.to_proplist (prune ~positive:true n_cond prop))
-  | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), args, loc, _)
+  | Sil.Call (ret_ids, Sil.Const (Const.Cfun callee_pname), args, loc, _)
     when Builtin.is_registered callee_pname ->
       let sym_exe_builtin = Builtin.get callee_pname in
       sym_exe_builtin (call_args prop_ callee_pname args ret_ids loc)
   | Sil.Call (ret_ids,
-              Sil.Const (Sil.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
+              Sil.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
               actual_params, loc, call_flags)
     when Config.lazy_dynamic_dispatch ->
       let norm_prop, norm_args = normalize_params current_pname prop_ actual_params in
@@ -1127,7 +1127,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       end
 
   | Sil.Call (ret_ids,
-              Sil.Const (Sil.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
+              Sil.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
               actual_params, loc, call_flags) ->
       do_error_checks (Paths.Path.curr_node path) instr current_pname current_pdesc;
       let norm_prop, norm_args = normalize_params current_pname prop_ actual_params in
@@ -1156,7 +1156,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
             proc_call summary (call_args norm_prop pname url_handled_args ret_ids loc) in
       IList.fold_left (fun acc pname -> exec_one_pname pname @ acc) [] resolved_pnames
 
-  | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags) ->
+  | Sil.Call (ret_ids, Sil.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) ->
       (** Generic fun call with known name *)
       let (prop_r, n_actual_params) = normalize_params current_pname prop_ actual_params in
       let resolved_pname =
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 59e63caac..4385d0da1 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -647,7 +647,7 @@ let prop_get_exn_name pname prop =
 let lookup_custom_errors prop =
   let rec search_error = function
     | [] -> None
-    | Sil.Hpointsto (Sil.Lvar var, Sil.Eexp (Sil.Const (Sil.Cstr error_str), _), _) :: _
+    | Sil.Hpointsto (Sil.Lvar var, Sil.Eexp (Sil.Const (Const.Cstr error_str), _), _) :: _
       when Pvar.equal var Sil.custom_error -> Some error_str
     | _ :: tl -> search_error tl in
   search_error (Prop.get_sigma prop)
@@ -721,7 +721,7 @@ let combine
     let handle_null_case_analysis sigma =
       let id_assigned_to_null id =
         let filter = function
-          | Sil.Aeq (Sil.Var id', Sil.Const (Sil.Cint i)) ->
+          | Sil.Aeq (Sil.Var id', Sil.Const (Const.Cint i)) ->
               Ident.equal id id' && IntLit.isnull i
           | _ -> false in
         IList.exists filter split.missing_pi in
@@ -1092,7 +1092,7 @@ let exe_spec
 
 let remove_constant_string_class prop =
   let filter = function
-    | Sil.Hpointsto (Sil.Const (Sil.Cstr _ | Sil.Cclass _), _, _) -> false
+    | Sil.Hpointsto (Sil.Const (Const.Cstr _ | Const.Cclass _), _, _) -> false
     | _ -> true in
   let sigma = IList.filter filter (Prop.get_sigma prop) in
   let sigmafp = IList.filter filter (Prop.get_sigma_footprint prop) in
diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml
index 57c6ea34d..f1f51dbbe 100644
--- a/infer/src/checkers/checkTraceCallSequence.ml
+++ b/infer/src/checkers/checkTraceCallSequence.ml
@@ -210,7 +210,7 @@ module Automaton = struct
   (** Transfer function for an instruction. *)
   let do_instr pn pd (instr : Sil.instr) (state : State.t) : State.t =
     match instr with
-    | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, loc, _) ->
+    | Sil.Call (_, Sil.Const (Const.Cfun callee_pn), _, loc, _) ->
         do_call pn pd callee_pn state loc
     | _ -> state
 
@@ -258,7 +258,7 @@ module BooleanVars = struct
       | instr -> instr in
 
     match normalize_instr instr with
-    | Sil.Prune (Sil.BinOp (Sil.Eq, _cond_e, Sil.Const (Sil.Cint i)), _, _, _)
+    | Sil.Prune (Sil.BinOp (Sil.Eq, _cond_e, Sil.Const (Const.Cint i)), _, _, _)
       when IntLit.iszero i ->
         let cond_e = Idenv.expand_expr idenv _cond_e in
         let state' = match exp_boolean_var cond_e with
@@ -267,7 +267,7 @@ module BooleanVars = struct
               State.prune state name false
           | None -> state in
         state'
-    | Sil.Prune (Sil.BinOp (Sil.Ne, _cond_e, Sil.Const (Sil.Cint i)), _, _, _)
+    | Sil.Prune (Sil.BinOp (Sil.Ne, _cond_e, Sil.Const (Const.Cint i)), _, _, _)
       when IntLit.iszero i ->
         let cond_e = Idenv.expand_expr idenv _cond_e in
         let state' = match exp_boolean_var cond_e with
@@ -281,7 +281,7 @@ module BooleanVars = struct
         let state' = match exp_boolean_var e1 with
           | Some name ->
               let b_opt = match e2 with
-                | Sil.Const (Sil.Cint i) -> Some (not (IntLit.iszero i))
+                | Sil.Const (Const.Cint i) -> Some (not (IntLit.iszero i))
                 | _ -> None in
               if verbose then
                 begin
diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml
index 675a2eaee..1ef9c65dc 100644
--- a/infer/src/checkers/checkers.ml
+++ b/infer/src/checkers/checkers.ml
@@ -282,7 +282,7 @@ let callback_check_write_to_parcel_java
     check_match (r_call_descs, w_call_descs) in
 
   let do_instr _ instr = match instr with
-    | Sil.Call (_, Sil.Const (Sil.Cfun _), (_this_exp, this_type):: _, _, _) ->
+    | Sil.Call (_, Sil.Const (Const.Cfun _), (_this_exp, this_type):: _, _, _) ->
         let this_exp = Idenv.expand_expr idenv _this_exp in
         if is_write_to_parcel this_exp this_type then begin
           if !verbose then
@@ -373,7 +373,7 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } =
       end in
 
   let do_instr _ instr = match instr with
-    | Sil.Call (_, Sil.Const (Sil.Cfun pn), (_arg1, _):: _, _, _) when is_nullcheck pn ->
+    | Sil.Call (_, Sil.Const (Const.Cfun pn), (_arg1, _):: _, _, _) when is_nullcheck pn ->
         let arg1 = Idenv.expand_expr idenv _arg1 in
         if is_formal_param arg1 then handle_check_of_formal arg1;
         if !verbose then
@@ -431,17 +431,17 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p
             when Pvar.equal p (Cfg.Procdesc.get_ret_var proc_desc') -> true
           | _ -> false in
         (match reverse_find_instr is_return_instr (Cfg.Procdesc.get_exit_node proc_desc') with
-         | Some (Sil.Set (_, _, Sil.Const (Sil.Cclass n), _)) -> Ident.name_to_string n
+         | Some (Sil.Set (_, _, Sil.Const (Const.Cclass n), _)) -> Ident.name_to_string n
          | _ -> "<" ^ (Procname.to_string proc_name') ^ ">")
     | None -> "?" in
 
   let get_actual_arguments node instr = match instr with
-    | Sil.Call (_, Sil.Const (Sil.Cfun _), _:: args, _, _) ->
+    | Sil.Call (_, Sil.Const (Const.Cfun _), _:: args, _, _) ->
         (try
            let find_const exp =
              let expanded = Idenv.expand_expr idenv exp in
              match expanded with
-             | Sil.Const (Sil.Cclass n) -> Ident.name_to_string n
+             | Sil.Const (Const.Cclass n) -> Ident.name_to_string n
              | Sil.Lvar _ -> (
                  let is_call_instr set call = match set, call with
                    | Sil.Set (_, _, Sil.Var (i1), _), Sil.Call (i2::[], _, _, _, _)
@@ -455,7 +455,8 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p
                  | Some s -> (
                      match reverse_find_instr (is_call_instr s) node with
                      (** Look for tmp := foo() *)
-                     | Some (Sil.Call (_, Sil.Const (Sil.Cfun pn), _, _, _)) -> get_return_const pn
+                     | Some (Sil.Call (_, Sil.Const (Const.Cfun pn), _, _, _)) ->
+                         get_return_const pn
                      | _ -> "?")
                  | _ -> "?")
              | _ -> "?" in
@@ -544,7 +545,7 @@ let callback_check_field_access { Callbacks.proc_desc } =
 (** Print c method calls. *)
 let callback_print_c_method_calls { Callbacks.proc_desc; proc_name } =
   let do_instr node = function
-    | Sil.Call (_, Sil.Const (Sil.Cfun pn), (e, _):: _, loc, _)
+    | Sil.Call (_, Sil.Const (Const.Cfun pn), (e, _):: _, loc, _)
       when Procname.is_c_method pn ->
         let receiver = match Errdesc.exp_rv_dexp node e with
           | Some de -> Sil.dexp_to_string de
@@ -557,7 +558,7 @@ let callback_print_c_method_calls { Callbacks.proc_desc; proc_name } =
           "CHECKERS_PRINT_OBJC_METHOD_CALLS"
           loc
           description
-    | Sil.Call (_, Sil.Const (Sil.Cfun pn), _, loc, _) ->
+    | Sil.Call (_, Sil.Const (Const.Cfun pn), _, loc, _) ->
         let description =
           Printf.sprintf "call to %s" (Procname.to_string pn) in
         ST.report_error
diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml
index 8f4ea1401..0d0a4dc37 100644
--- a/infer/src/checkers/codeQuery.ml
+++ b/infer/src/checkers/codeQuery.ml
@@ -161,7 +161,7 @@ module Match = struct
 
   let rec match_query show env idenv caller_pn (rule, action) proc_name node instr =
     match rule, instr with
-    | CodeQueryAst.Call (ae1, ae2), Sil.Call (_, Sil.Const (Sil.Cfun pn), _, loc, _) ->
+    | CodeQueryAst.Call (ae1, ae2), Sil.Call (_, Sil.Const (Const.Cfun pn), _, loc, _) ->
         if exp_match env ae1 (Vfun caller_pn) && exp_match env ae2 (Vfun pn) then
           begin
             if show then print_action env action proc_name node loc;
@@ -170,7 +170,7 @@ module Match = struct
         else false
     | CodeQueryAst.Call _, _ -> false
     | CodeQueryAst.MethodCall (ae1, ae2, ael_opt),
-      Sil.Call (_, Sil.Const (Sil.Cfun pn), (_e1, _):: params, loc, { Sil.cf_virtual = true }) ->
+      Sil.Call (_, Sil.Const (Const.Cfun pn), (_e1, _):: params, loc, { Sil.cf_virtual = true }) ->
         let e1 = Idenv.expand_expr idenv _e1 in
         let vl = IList.map (function _e, _ -> Vval (Idenv.expand_expr idenv _e)) params in
         if exp_match env ae1 (Vval e1) && exp_match env ae2 (Vfun pn) && opt_match exp_list_match env ael_opt vl then
diff --git a/infer/src/checkers/constantPropagation.ml b/infer/src/checkers/constantPropagation.ml
index 986d55fbd..3fa6bb212 100644
--- a/infer/src/checkers/constantPropagation.ml
+++ b/infer/src/checkers/constantPropagation.ml
@@ -18,7 +18,7 @@ let verbose = false
 (* Merge two constant maps by adding keys as necessary *)
 let merge_values _ c1_opt c2_opt =
   match c1_opt, c2_opt with
-  | Some (Some c1), Some (Some c2) when Sil.const_equal c1 c2 -> Some (Some c1)
+  | Some (Some c1), Some (Some c2) when Const.equal c1 c2 -> Some (Some c1)
   | Some c, None
   | None, Some c -> Some c
   | _ -> Some None
@@ -27,12 +27,12 @@ module ConstantMap = Sil.ExpMap
 
 (** Dataflow struct *)
 module ConstantFlow = Dataflow.MakeDF(struct
-    type t = (Sil.const option) ConstantMap.t
+    type t = (Const.t option) ConstantMap.t
 
     let pp fmt constants =
       let pp_key fmt = Sil.pp_exp pe_text fmt in
       let print_kv k = function
-        | Some v -> Format.fprintf fmt "  %a -> %a@." pp_key k (Sil.pp_const pe_text) v
+        | Some v -> Format.fprintf fmt "  %a -> %a@." pp_key k (Const.pp pe_text) v
         | _ -> Format.fprintf fmt "  %a -> None@." pp_key k in
       Format.fprintf fmt "[@.";
       ConstantMap.iter print_kv constants;
@@ -40,8 +40,8 @@ module ConstantFlow = Dataflow.MakeDF(struct
 
     (* Item - wise equality where values are equal iff
        - both are None
-       - both are a constant and equal wrt. Sil.const_equal *)
-    let equal m n = ConstantMap.equal (opt_equal Sil.const_equal) m n
+       - both are a constant and equal wrt. Const.equal *)
+    let equal m n = ConstantMap.equal (opt_equal Const.equal) m n
 
     let join = ConstantMap.merge merge_values
 
@@ -79,28 +79,29 @@ module ConstantFlow = Dataflow.MakeDF(struct
               update (Sil.Lvar p) (ConstantMap.find (Sil.Var i) constants) constants
 
           (* Handle propagation of string with StringBuilder. Does not handle null case *)
-          | Sil.Call (_, Sil.Const (Sil.Cfun pn), (Sil.Var sb, _):: [], _, _)
+          | Sil.Call (_, Sil.Const (Const.Cfun pn), (Sil.Var sb, _):: [], _, _)
             when has_class pn "java.lang.StringBuilder"
               && has_method pn "<init>" ->  (* StringBuilder.<init> *)
-              update (Sil.Var sb) (Some (Sil.Cstr "")) constants
+              update (Sil.Var sb) (Some (Const.Cstr "")) constants
 
-          | Sil.Call (i:: [], Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: [], _, _)
+          | Sil.Call (i:: [], Sil.Const (Const.Cfun pn), (Sil.Var i1, _):: [], _, _)
             when has_class pn "java.lang.StringBuilder"
               && has_method pn "toString" -> (* StringBuilder.toString *)
               update (Sil.Var i) (ConstantMap.find (Sil.Var i1) constants) constants
 
-          | Sil.Call (i:: [], Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: (Sil.Var i2, _):: [], _, _)
+          | Sil.Call
+              (i:: [], Sil.Const (Const.Cfun pn), (Sil.Var i1, _):: (Sil.Var i2, _):: [], _, _)
             when has_class pn "java.lang.StringBuilder"
               && has_method pn "append" -> (* StringBuilder.append *)
               (match
                  ConstantMap.find (Sil.Var i1) constants,
                  ConstantMap.find (Sil.Var i2) constants with
-              | Some (Sil.Cstr s1), Some (Sil.Cstr s2) ->
+              | Some (Const.Cstr s1), Some (Const.Cstr s2) ->
                   begin
                     let s = s1 ^ s2 in
                     let u =
                       if String.length s < string_widening_limit then
-                        Some (Sil.Cstr s)
+                        Some (Const.Cstr s)
                       else
                         None in
                     update (Sil.Var i) u constants
@@ -135,7 +136,7 @@ let run tenv proc_desc =
     | ConstantFlow.Dead_state -> ConstantMap.empty in
   get_constants
 
-type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option
+type const_map = Cfg.Node.t -> Sil.exp -> Const.t option
 
 (** Build a const map lazily. *)
 let build_const_map tenv pdesc =
diff --git a/infer/src/checkers/constantPropagation.mli b/infer/src/checkers/constantPropagation.mli
index ce85c8d16..15cbed6c1 100644
--- a/infer/src/checkers/constantPropagation.mli
+++ b/infer/src/checkers/constantPropagation.mli
@@ -9,7 +9,7 @@
 
 open! Utils
 
-type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option
+type const_map = Cfg.Node.t -> Sil.exp -> Const.t option
 
 (** Build a const map lazily. *)
 val build_const_map : Tenv.t -> Cfg.Procdesc.t -> const_map
diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml
index 3fa2c31d4..58d5cc93f 100644
--- a/infer/src/checkers/dataflow.ml
+++ b/infer/src/checkers/dataflow.ml
@@ -51,12 +51,12 @@ let node_throws node (proc_throws : Procname.t -> throws) : throws =
     | Sil.Set (Sil.Lvar pvar, _, Sil.Exn _, _) when is_return pvar ->
         (* assignment to return variable is an artifact of a throw instruction *)
         Throws
-    | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, _, _)
+    | Sil.Call (_, Sil.Const (Const.Cfun callee_pn), _, _, _)
       when Builtin.is_registered callee_pn ->
         if Procname.equal callee_pn ModelBuiltins.__cast
         then DontKnow
         else DoesNotThrow
-    | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, _, _) ->
+    | Sil.Call (_, Sil.Const (Const.Cfun callee_pn), _, _, _) ->
         proc_throws callee_pn
     | _ ->
         DoesNotThrow in
diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml
index 435c92f98..8ed8dc411 100644
--- a/infer/src/checkers/patternMatch.ml
+++ b/infer/src/checkers/patternMatch.ml
@@ -165,11 +165,11 @@ let get_field_type_name
   | _ -> None
 
 let java_get_const_type_name
-    (const: Sil.const): string =
+    (const: Const.t): string =
   match const with
-  | Sil.Cstr _ -> "java.lang.String"
-  | Sil.Cint _ -> "java.lang.Integer"
-  | Sil.Cfloat _ -> "java.lang.Double"
+  | Const.Cstr _ -> "java.lang.String"
+  | Const.Cint _ -> "java.lang.Integer"
+  | Const.Cfloat _ -> "java.lang.Double"
   | _ -> "_"
 
 let get_vararg_type_names
@@ -178,7 +178,7 @@ let get_vararg_type_names
   (* Is this the node creating ivar? *)
   let rec initializes_array instrs =
     match instrs with
-    | Sil.Call ([t1], Sil.Const (Sil.Cfun pn), _, _, _)::
+    | Sil.Call ([t1], Sil.Const (Const.Cfun pn), _, _, _)::
       Sil.Set (Sil.Lvar iv, _, Sil.Var t2, _):: is ->
         (Pvar.equal ivar iv && Ident.equal t1 t2 &&
          Procname.equal pn (Procname.from_string_c_fun "__new_array"))
@@ -252,7 +252,7 @@ let get_java_field_access_signature = function
 (** Returns the formal signature (class name, method name,
     argument type names and return type name) *)
 let get_java_method_call_formal_signature = function
-  | Sil.Call (_, Sil.Const (Sil.Cfun pn), (_, tt):: args, _, _) ->
+  | Sil.Call (_, Sil.Const (Const.Cfun pn), (_, tt):: args, _, _) ->
       (match pn with
        | Procname.Java pn_java ->
            let arg_names = IList.map (function | _, t -> get_type_name t) args in
@@ -333,7 +333,7 @@ let java_get_vararg_values node pvar idenv =
 let proc_calls resolve_attributes pdesc filter : (Procname.t * ProcAttributes.t) list =
   let res = ref [] in
   let do_instruction _ instr = match instr with
-    | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, _, _) ->
+    | Sil.Call (_, Sil.Const (Const.Cfun callee_pn), _, _, _) ->
         begin
           match resolve_attributes callee_pn with
           | Some callee_attributes ->
diff --git a/infer/src/checkers/patternMatch.mli b/infer/src/checkers/patternMatch.mli
index bf2733d0d..d3155e9c8 100644
--- a/infer/src/checkers/patternMatch.mli
+++ b/infer/src/checkers/patternMatch.mli
@@ -66,7 +66,7 @@ val strict_supertype_iter : Tenv.t -> (Typ.struct_typ -> unit) -> Typ.struct_typ
 val strict_supertype_exists : Tenv.t -> (Typ.struct_typ -> bool) -> Typ.struct_typ -> bool
 
 (** Get the name of the type of a constant *)
-val java_get_const_type_name : Sil.const -> string
+val java_get_const_type_name : Const.t -> string
 
 (** Get the values of a vararg parameter given the pvar used to assign the elements. *)
 val java_get_vararg_values : Cfg.Node.t -> Pvar.t -> Idenv.t -> Sil.exp list
diff --git a/infer/src/checkers/printfArgs.ml b/infer/src/checkers/printfArgs.ml
index 0cf20b5cf..592327f4b 100644
--- a/infer/src/checkers/printfArgs.ml
+++ b/infer/src/checkers/printfArgs.ml
@@ -88,7 +88,7 @@ let format_arguments
     (args: (Sil.exp * Typ.t) list): (string option * (Sil.exp list) * (Sil.exp option)) =
 
   let format_string = match IList.nth args printf.format_pos with
-    | Sil.Const (Sil.Cstr fmt), _ -> Some fmt
+    | Sil.Const (Const.Cstr fmt), _ -> Some fmt
     | _ -> None in
 
   let fixed_nvars = IList.map
@@ -175,7 +175,7 @@ let check_printf_args_ok
     | _ -> raise (Failure "Could not resolve fixed type name") in
 
   match instr with
-  | Sil.Call (_, Sil.Const (Sil.Cfun pn), args, cl, _) -> (
+  | Sil.Call (_, Sil.Const (Const.Cfun pn), args, cl, _) -> (
       match printf_like_function pn with
       | Some printf -> (
           try
diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml
index 51f20006c..5acadc457 100644
--- a/infer/src/checkers/repeatedCallsChecker.ml
+++ b/infer/src/checkers/repeatedCallsChecker.ml
@@ -73,7 +73,7 @@ struct
         Procname.equal pn ModelBuiltins.__new_array in
       let do_instr instr =
         match instr with
-        | Sil.Call (_, Sil.Const (Sil.Cfun pn), _, loc, _) when proc_is_new pn ->
+        | Sil.Call (_, Sil.Const (Const.Cfun pn), _, loc, _) when proc_is_new pn ->
             found := Some loc
         | _ -> () in
       IList.iter do_instr (Cfg.Node.get_instrs node);
@@ -118,11 +118,11 @@ struct
       IList.for_all filter_arg args in
 
     match instr with
-    | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _, loc, call_flags)
+    | Sil.Call (ret_ids, Sil.Const (Const.Cfun callee_pname), _, loc, call_flags)
       when ret_ids <> [] && arguments_not_temp normalized_etl ->
         let instr_normalized_args = Sil.Call (
             ret_ids,
-            Sil.Const (Sil.Cfun callee_pname),
+            Sil.Const (Const.Cfun callee_pname),
             normalized_etl,
             loc,
             call_flags) in
diff --git a/infer/src/checkers/sqlChecker.ml b/infer/src/checkers/sqlChecker.ml
index 00c4d7c65..7014d5df5 100644
--- a/infer/src/checkers/sqlChecker.ml
+++ b/infer/src/checkers/sqlChecker.ml
@@ -38,7 +38,7 @@ let callback_sql { Callbacks.proc_desc; proc_name; tenv } =
           begin
             let matches s r = Str.string_match r s 0 in
             match const_map node rvar1, const_map node rvar2 with
-            | Some (Sil.Cstr ""), Some (Sil.Cstr s2) ->
+            | Some (Const.Cstr ""), Some (Const.Cstr s2) ->
                 if IList.exists (matches s2) sql_start then
                   begin
                     L.stdout
@@ -53,7 +53,7 @@ let callback_sql { Callbacks.proc_desc; proc_name; tenv } =
         end in
 
     match instr with
-    | Sil.Call (_, Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: (Sil.Var i2, _):: [], l, _) ->
+    | Sil.Call (_, Sil.Const (Const.Cfun pn), (Sil.Var i1, _):: (Sil.Var i2, _):: [], l, _) ->
         begin
           match pn with
           | Procname.Java pn_java ->
diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml
index f2641c80c..3ed6cf7a0 100644
--- a/infer/src/clang/cArithmetic_trans.ml
+++ b/infer/src/clang/cArithmetic_trans.ml
@@ -26,7 +26,7 @@ let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl =
   let release_pname = ModelBuiltins.__objc_release in
   let autorelease_pname = ModelBuiltins.__set_autorelease_attribute in
   let mk_call procname e t =
-    let bi_retain = Sil.Const (Sil.Cfun procname) in
+    let bi_retain = Sil.Const (Const.Cfun procname) in
     Sil.Call([], bi_retain, [(e, t)], loc, Sil.cf_default) in
   match typ with
   | Typ.Tptr (_, Typ.Pk_pointer) when not rhs_owning_method && not is_e1_decl ->
@@ -144,12 +144,12 @@ let unary_operation_instruction uoi e typ loc =
   | `PostInc ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Letderef (id, e, typ, loc) in
-      let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
+      let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Const.Cint (IntLit.one))) in
       (Sil.Var id, instr1::[Sil.Set (e, typ, e_plus_1, loc)])
   | `PreInc ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Letderef (id, e, typ, loc) in
-      let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
+      let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Const.Cint (IntLit.one))) in
       let exp = if General_utils.is_cpp_translation Config.clang_lang then
           e
         else
@@ -158,12 +158,12 @@ let unary_operation_instruction uoi e typ loc =
   | `PostDec ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Letderef (id, e, typ, loc) in
-      let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
+      let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Const.Cint (IntLit.one))) in
       (Sil.Var id, instr1::[Sil.Set (e, typ, e_minus_1, loc)])
   | `PreDec ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Letderef (id, e, typ, loc) in
-      let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
+      let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Const.Cint (IntLit.one))) in
       let exp = if General_utils.is_cpp_translation Config.clang_lang then
           e
         else
@@ -219,6 +219,6 @@ let bin_op_to_string boi =
 
 let sil_const_plus_one const =
   match const with
-  | Sil.Const (Sil.Cint n) ->
-      Sil.Const (Sil.Cint (IntLit.add n IntLit.one))
-  | _ -> Sil.BinOp (Sil.PlusA, const, Sil.Const (Sil.Cint (IntLit.one)))
+  | Sil.Const (Const.Cint n) ->
+      Sil.Const (Const.Cint (IntLit.add n IntLit.one))
+  | _ -> Sil.BinOp (Sil.PlusA, const, Sil.Const (Const.Cint (IntLit.one)))
diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml
index 6a3efdfac..fc9f280d3 100644
--- a/infer/src/clang/cTrans.ml
+++ b/infer/src/clang/cTrans.ml
@@ -84,7 +84,7 @@ struct
       let fname = ModelBuiltins.__set_autorelease_attribute in
       let ret_id = Ident.create_fresh Ident.knormal in
       let stmt_call =
-        Sil.Call ([ret_id], (Sil.Const (Sil.Cfun fname)), [(exp, typ)], sil_loc, Sil.cf_default) in
+        Sil.Call ([ret_id], Sil.Const (Const.Cfun fname), [(exp, typ)], sil_loc, Sil.cf_default) in
       [stmt_call]
     else []
 
@@ -330,7 +330,7 @@ struct
 
   let stringLiteral_trans trans_state expr_info str =
     let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
-    let exp = Sil.Const (Sil.Cstr (str)) in
+    let exp = Sil.Const (Const.Cstr (str)) in
     { empty_res_trans with exps = [(exp, typ)]}
 
   (* FROM CLANG DOCS: "Implements the GNU __null extension,
@@ -343,7 +343,7 @@ struct
      So we implement it as the constant zero *)
   let gNUNullExpr_trans trans_state expr_info =
     let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
-    let exp = Sil.Const (Sil.Cint (IntLit.zero)) in
+    let exp = Sil.Const (Const.Cint (IntLit.zero)) in
     { empty_res_trans with exps = [(exp, typ)]}
 
   let nullPtrExpr_trans trans_state expr_info =
@@ -364,7 +364,7 @@ struct
 
   let characterLiteral_trans trans_state expr_info n =
     let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
-    let exp = Sil.Const (Sil.Cint (IntLit.of_int n)) in
+    let exp = Sil.Const (Const.Cint (IntLit.of_int n)) in
     { empty_res_trans with exps = [(exp, typ)]}
 
   let booleanValue_trans trans_state expr_info b =
@@ -372,7 +372,7 @@ struct
 
   let floatingLiteral_trans trans_state expr_info float_string =
     let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
-    let exp = Sil.Const (Sil.Cfloat (float_of_string float_string)) in
+    let exp = Sil.Const (Const.Cfloat (float_of_string float_string)) in
     { empty_res_trans with exps = [(exp, typ)]}
 
   (* Note currently we don't have support for different qual     *)
@@ -399,7 +399,7 @@ struct
     let zero_opt = match typ with
       | Typ.Tfloat _  | Typ.Tptr _ | Typ.Tint _ -> Some (Sil.zero_value_of_numerical_type typ)
       | Typ.Tvoid -> None
-      | _ -> Some (Sil.Const (Sil.Cint IntLit.zero)) in
+      | _ -> Some (Sil.Const (Const.Cint IntLit.zero)) in
     match zero_opt with
     | Some zero -> { empty_res_trans with exps = [(zero, typ)] }
     | _ -> empty_res_trans
@@ -466,11 +466,11 @@ struct
       else Procname.from_string_c_fun name in
     let is_builtin = Builtin.is_registered non_mangled_func_name in
     if is_builtin then (* malloc, free, exit, scanf, ... *)
-      { empty_res_trans with exps = [(Sil.Const (Sil.Cfun non_mangled_func_name), typ)] }
+      { empty_res_trans with exps = [(Sil.Const (Const.Cfun non_mangled_func_name), typ)] }
     else
       begin
         if address_of_function then Cfg.set_procname_priority context.cfg pname;
-        { empty_res_trans with exps = [(Sil.Const (Sil.Cfun pname), typ)] }
+        { empty_res_trans with exps = [(Sil.Const (Const.Cfun pname), typ)] }
       end
 
   let var_deref_trans trans_state stmt_info decl_ref =
@@ -587,7 +587,7 @@ struct
     (* unlike field access, for method calls there is no need to expand class type *)
     let pname = CMethod_trans.create_procdesc_with_pointer context decl_ptr (Some class_name)
         method_name type_ptr in
-    let method_exp = (Sil.Const (Sil.Cfun pname), method_typ) in
+    let method_exp = (Sil.Const (Const.Cfun pname), method_typ) in
     Cfg.set_procname_priority context.CContext.cfg pname;
     { pre_trans_result with
       is_cpp_call_virtual = is_cpp_virtual;
@@ -679,7 +679,7 @@ struct
 
   (* get the sil value of the enum constant from the map or by evaluating it *)
   and get_enum_constant_expr context enum_constant_pointer =
-    let zero = Sil.Const (Sil.Cint IntLit.zero) in
+    let zero = Sil.Const (Const.Cint IntLit.zero) in
     try
       let (prev_enum_constant_opt, sil_exp_opt) =
         Ast_utils.get_enum_constant_exp enum_constant_pointer in
@@ -828,7 +828,7 @@ struct
          Returning -1. NEED TO BE FIXED" in
     let callee_pname_opt =
       match sil_fe with
-      | Sil.Const (Sil.Cfun pn) ->
+      | Sil.Const (Const.Cfun pn) ->
           Some pn
       | _ -> None (* function pointer *) in
     let should_translate_args =
@@ -857,7 +857,7 @@ struct
                  NEED TO BE FIXED\n\n";
               fix_param_exps_mismatch params_stmt params) in
       let act_params = if is_cf_retain_release then
-          (Sil.Const (Sil.Cint IntLit.one), Typ.Tint Typ.IBool) :: act_params
+          (Sil.Const (Const.Cint IntLit.one), Typ.Tint Typ.IBool) :: act_params
         else act_params in
       match
         CTrans_utils.builtin_trans trans_state_pri sil_loc si function_type callee_pname_opt with
@@ -902,7 +902,7 @@ struct
     assert ((IList.length result_trans_callee.exps) = 2);
     let (sil_method, _) = IList.hd result_trans_callee.exps in
     let callee_pname = match sil_method with
-      | Sil.Const (Sil.Cfun pn) -> pn
+      | Sil.Const (Const.Cfun pn) -> pn
       | _ -> assert false (* method pointer not implemented, this shouldn't happen *) in
     if CTrans_models.is_assert_log sil_method then
       CTrans_utils.trans_assertion sil_loc context trans_state_pri.succ_nodes
@@ -1067,7 +1067,7 @@ struct
                                 instrs = instr_block_param;
                               } in
         let call_flags = { Sil.cf_default with Sil.cf_virtual = is_virtual; } in
-        let method_sil = Sil.Const (Sil.Cfun callee_name) in
+        let method_sil = Sil.Const (Const.Cfun callee_name) in
         let res_trans_call = create_call_instr trans_state method_type method_sil param_exps
             sil_loc call_flags ~is_objc_method:true in
         let selector = obj_c_message_expr_info.Clang_ast_t.omei_selector in
@@ -1187,7 +1187,7 @@ struct
       Printing.log_out " No short-circuit condition\n";
       let res_trans_cond =
         if is_null_stmt cond then {
-          empty_res_trans with exps = [(Sil.Const (Sil.Cint IntLit.one), (Typ.Tint Typ.IBool))]
+          empty_res_trans with exps = [(Sil.Const (Const.Cint IntLit.one), (Typ.Tint Typ.IBool))]
         }
         (* Assumption: If it's a null_stmt, it is a loop with no bound, so we set condition to 1 *)
         else
@@ -1976,7 +1976,7 @@ struct
     let ret_id = Ident.create_fresh Ident.knormal in
     let autorelease_pool_vars = CVar_decl.compute_autorelease_pool_vars context stmts in
     let stmt_call =
-      Sil.Call([ret_id], (Sil.Const (Sil.Cfun fname)),
+      Sil.Call([ret_id], (Sil.Const (Const.Cfun fname)),
                autorelease_pool_vars, sil_loc, Sil.cf_default) in
     let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") in
     let call_node = create_node node_kind [stmt_call] sil_loc context in
@@ -2039,7 +2039,7 @@ struct
     let (var_exp_inside, typ_inside) = match typ with
       | Typ.Tarray (t, _)
       | Typ.Tptr (t, _) when Typ.is_array_of_cpp_class typ || is_dyn_array ->
-          Sil.Lindex (var_exp, Sil.Const (Sil.Cint (IntLit.of_int n))), t
+          Sil.Lindex (var_exp, Sil.Const (Const.Cint (IntLit.of_int n))), t
       | _ -> var_exp, typ in
     let trans_state' = { trans_state with var_exp_typ = Some (var_exp_inside, typ_inside) } in
     match stmts with
@@ -2090,7 +2090,7 @@ struct
             (match res_trans_size.exps with
              | [(exp, _)] -> Some exp, res_trans_size
              | _ -> None, empty_res_trans)
-        | None -> Some (Sil.Const (Sil.Cint (IntLit.minus_one))), empty_res_trans
+        | None -> Some (Sil.Const (Const.Cint (IntLit.minus_one))), empty_res_trans
       else None, empty_res_trans in
     let res_trans_new = cpp_new_trans trans_state_pri sil_loc typ size_exp_opt in
     let stmt_opt = Ast_utils.get_stmt_opt cxx_new_expr_info.Clang_ast_t.xnei_initializer_expr in
@@ -2104,8 +2104,8 @@ struct
       if is_dyn_array && Typ.is_pointer_to_cpp_class typ then
         let rec create_stmts stmt_opt size_exp_opt =
           match stmt_opt, size_exp_opt with
-          | Some stmt, Some (Sil.Const (Sil.Cint n)) when not (IntLit.iszero n) ->
-              let n_minus_1 = Some ((Sil.Const (Sil.Cint (IntLit.sub n IntLit.one)))) in
+          | Some stmt, Some (Sil.Const (Const.Cint n)) when not (IntLit.iszero n) ->
+              let n_minus_1 = Some ((Sil.Const (Const.Cint (IntLit.sub n IntLit.one)))) in
               stmt :: create_stmts stmt_opt n_minus_1
           | _ -> [] in
         let stmts = create_stmts stmt_opt size_exp_opt in
@@ -2133,7 +2133,7 @@ struct
     let result_trans_param = exec_with_self_exception instruction trans_state_param param in
     let exp = extract_exp_from_list result_trans_param.exps
         "WARNING: There should be one expression to delete. \n" in
-    let call_instr = Sil.Call ([], (Sil.Const (Sil.Cfun fname)), [exp], sil_loc, Sil.cf_default) in
+    let call_instr = Sil.Call ([], Sil.Const (Const.Cfun fname), [exp], sil_loc, Sil.cf_default) in
     let call_res_trans = { empty_res_trans with instrs = [call_instr] } in
     let all_res_trans = if false then
         (* FIXME (t10135167): call destructor on deleted pointer if it's not null *)
@@ -2187,7 +2187,7 @@ struct
     let sizeof_expr = match cast_type with
       | Typ.Tptr (typ, _) -> Sil.Sizeof (typ, None, subtypes)
       | _ -> assert false in
-    let builtin = Sil.Const (Sil.Cfun ModelBuiltins.__cast) in
+    let builtin = Sil.Const (Const.Cfun ModelBuiltins.__cast) in
     let stmt = match stmts with [stmt] -> stmt | _ -> assert false in
     let res_trans_stmt = exec_with_glvalue_as_reference instruction trans_state' stmt in
     let exp = match res_trans_stmt.exps with | [e] -> e | _ -> assert false in
@@ -2215,7 +2215,7 @@ struct
       IList.map (exec_with_glvalue_as_reference instruction trans_state_param) stmts in
     let params = collect_exprs res_trans_subexpr_list  in
     let fun_name = Procname.from_string_c_fun CFrontend_config.infer_skip_gcc_ast_stmt in
-    let sil_fun = Sil.Const (Sil.Cfun fun_name) in
+    let sil_fun = Sil.Const (Const.Cfun fun_name) in
     let call_instr = Sil.Call ([], sil_fun, params, sil_loc, Sil.cf_default) in
     let res_trans_call = { empty_res_trans with
                            instrs = [call_instr];
@@ -2227,7 +2227,7 @@ struct
 
   and cxxPseudoDestructorExpr_trans () =
     let fun_name = Procname.from_string_c_fun CFrontend_config.infer_skip_fun in
-    { empty_res_trans with exps = [(Sil.Const (Sil.Cfun fun_name), Typ.Tvoid)] }
+    { empty_res_trans with exps = [(Sil.Const (Const.Cfun fun_name), Typ.Tvoid)] }
 
   and cxxTypeidExpr_trans trans_state stmt_info stmts expr_info =
     let tenv = trans_state.context.CContext.tenv in
@@ -2241,7 +2241,7 @@ struct
           instruction trans_state_param stmt
       | _ -> empty_res_trans in
     let fun_name = ModelBuiltins.__cxx_typeid in
-    let sil_fun = Sil.Const (Sil.Cfun fun_name) in
+    let sil_fun = Sil.Const (Const.Cfun fun_name) in
     let ret_id = Ident.create_fresh Ident.knormal in
     let type_info_objc = (Sil.Sizeof (typ, None, Sil.Subtype.exact), Typ.Tvoid) in
     let field_name_decl = Ast_utils.make_qual_name_decl ["type_info"; "std"] "__type_name" in
@@ -2269,7 +2269,7 @@ struct
     let trans_state_param = { trans_state_pri with succ_nodes = [] } in
     let res_trans_subexpr_list = IList.map (instruction trans_state_param) stmts in
     let params = collect_exprs res_trans_subexpr_list  in
-    let sil_fun = Sil.Const (Sil.Cfun fun_name) in
+    let sil_fun = Sil.Const (Const.Cfun fun_name) in
     let ret_id = Ident.create_fresh Ident.knormal in
     let ret_exp = Sil.Var ret_id in
     let call_instr = Sil.Call ([ret_id], sil_fun, params, sil_loc, Sil.cf_default) in
diff --git a/infer/src/clang/cTrans_models.ml b/infer/src/clang/cTrans_models.ml
index ba7327371..5ed568b27 100644
--- a/infer/src/clang/cTrans_models.ml
+++ b/infer/src/clang/cTrans_models.ml
@@ -107,19 +107,20 @@ let builtin_predefined_model fun_stmt sil_fe =
   | Some typ ->
       let typ = Ast_utils.string_of_type_ptr typ in
       (match sil_fe with
-       | Sil.Const (Sil.Cfun pn) when Specs.summary_exists pn -> sil_fe, false
-       | Sil.Const (Sil.Cfun pn) when is_retain_predefined_model typ (Procname.to_string pn) ->
-           Sil.Const (Sil.Cfun ModelBuiltins.__objc_retain_cf) , true
-       | Sil.Const (Sil.Cfun pn) when is_release_predefined_model typ (Procname.to_string pn) ->
-           Sil.Const (Sil.Cfun ModelBuiltins.__objc_release_cf), true
+       | Sil.Const (Const.Cfun pn) when Specs.summary_exists pn -> sil_fe, false
+       | Sil.Const (Const.Cfun pn) when is_retain_predefined_model typ (Procname.to_string pn) ->
+           Sil.Const (Const.Cfun ModelBuiltins.__objc_retain_cf) , true
+       | Sil.Const (Const.Cfun pn) when is_release_predefined_model typ (Procname.to_string pn) ->
+           Sil.Const (Const.Cfun ModelBuiltins.__objc_release_cf), true
        | _ -> sil_fe, false)
   | _ -> sil_fe, false
 
 (** If the function is a builtin model, return the model, otherwise return the function *)
 let is_assert_log sil_fe =
   match sil_fe with
-  | Sil.Const (Sil.Cfun (Procname.ObjC_Cpp _ as pn)) -> is_assert_log_method (Procname.to_string pn)
-  | Sil.Const (Sil.Cfun (Procname.C _ as pn)) -> is_assert_log_s (Procname.to_string pn)
+  | Sil.Const (Const.Cfun (Procname.ObjC_Cpp _ as pn)) ->
+      is_assert_log_method (Procname.to_string pn)
+  | Sil.Const (Const.Cfun (Procname.C _ as pn)) -> is_assert_log_s (Procname.to_string pn)
   | _ -> false
 
 
diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml
index 29684bde0..d0b2441c3 100644
--- a/infer/src/clang/cTrans_utils.ml
+++ b/infer/src/clang/cTrans_utils.ml
@@ -302,11 +302,11 @@ let create_alloc_instrs context sil_loc function_type fname size_exp_opt procnam
     | None -> sizeof_exp_ in
   let exp = (sizeof_exp, Typ.Tint Typ.IULong) in
   let procname_arg = match procname_opt with
-    | Some procname -> [Sil.Const (Sil.Cfun (procname)), Typ.Tvoid]
+    | Some procname -> [Sil.Const (Const.Cfun (procname)), Typ.Tvoid]
     | None -> [] in
   let args = exp :: procname_arg in
   let ret_id = Ident.create_fresh Ident.knormal in
-  let stmt_call = Sil.Call([ret_id], (Sil.Const (Sil.Cfun fname)), args, sil_loc, Sil.cf_default) in
+  let stmt_call = Sil.Call([ret_id], Sil.Const (Const.Cfun fname), args, sil_loc, Sil.cf_default) in
   (function_type, stmt_call, Sil.Var ret_id)
 
 let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc procname_opt =
@@ -332,7 +332,8 @@ let objc_new_trans trans_state loc stmt_info cls_name function_type =
   let pname = General_utils.mk_procname_from_objc_method cls_name CFrontend_config.init Procname.Instance_objc_method in
   CMethod_trans.create_external_procdesc trans_state.context.CContext.cfg pname is_instance None;
   let args = [(alloc_ret_exp, alloc_ret_type)] in
-  let init_stmt_call = Sil.Call([init_ret_id], (Sil.Const (Sil.Cfun pname)), args, loc, call_flags) in
+  let init_stmt_call =
+    Sil.Call ([init_ret_id], Sil.Const (Const.Cfun pname), args, loc, call_flags) in
   let instrs = [alloc_stmt_call; init_stmt_call] in
   let res_trans_tmp = { empty_res_trans with instrs = instrs } in
   let res_trans =
@@ -369,7 +370,8 @@ let create_cast_instrs context exp cast_from_typ cast_to_typ sil_loc =
   let sizeof_exp = Sil.Sizeof (cast_typ_no_pointer, None, Sil.Subtype.exact) in
   let pname = ModelBuiltins.__objc_cast in
   let args = [(exp, cast_from_typ); (sizeof_exp, Typ.Tint Typ.IULong)] in
-  let stmt_call = Sil.Call([ret_id], (Sil.Const (Sil.Cfun pname)), args, sil_loc, Sil.cf_default) in
+  let stmt_call =
+    Sil.Call ([ret_id], Sil.Const (Const.Cfun pname), args, sil_loc, Sil.cf_default) in
   (stmt_call, Sil.Var ret_id)
 
 let cast_trans context exps sil_loc callee_pname_opt function_type =
@@ -440,8 +442,8 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged =
       ([], (exp, cast_typ))
 
 let trans_assertion_failure sil_loc context =
-  let assert_fail_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__infer_fail) in
-  let args = [Sil.Const (Sil.Cstr Config.default_failure_name), Typ.Tvoid] in
+  let assert_fail_builtin = Sil.Const (Const.Cfun ModelBuiltins.__infer_fail) in
+  let args = [Sil.Const (Const.Cstr Config.default_failure_name), Typ.Tvoid] in
   let call_instr = Sil.Call ([], assert_fail_builtin, args, sil_loc, Sil.cf_default) in
   let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context)
   and failure_node =
@@ -688,7 +690,7 @@ let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero =
         let size = IntLit.to_int n in
         let indices = list_range 0 (size - 1) in
         let index_constants =
-          IList.map (fun i -> (Sil.Const (Sil.Cint (IntLit.of_int i)))) indices in
+          IList.map (fun i -> (Sil.Const (Const.Cint (IntLit.of_int i)))) indices in
         let lh_exprs =
           IList.map (fun index_expr -> Sil.Lindex (e, index_expr)) index_constants in
         let lh_types = replicate size arrtyp in
diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml
index e9a2e4dbf..68a1cb3c5 100644
--- a/infer/src/eradicate/eradicateChecks.ml
+++ b/infer/src/eradicate/eradicateChecks.ml
@@ -140,7 +140,7 @@ let check_condition case_zero find_canonical_duplicate curr_pname
           Mangled.equal c throwable_class
       | _ -> false in
     let do_instr = function
-      | Sil.Call (_, Sil.Const (Sil.Cfun pn), [_; (Sil.Sizeof(t, _, _), _)], _, _) when
+      | Sil.Call (_, Sil.Const (Const.Cfun pn), [_; (Sil.Sizeof(t, _, _), _)], _, _) when
           Procname.equal pn ModelBuiltins.__instanceof && typ_is_throwable t ->
           throwable_found := true
       | _ -> () in
diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml
index a38900173..6853b9b1d 100644
--- a/infer/src/eradicate/typeCheck.ml
+++ b/infer/src/eradicate/typeCheck.ml
@@ -98,10 +98,10 @@ module ComplexExpressions = struct
           dexp_to_string de ^ "." ^ Ident.fieldname_to_string f
       | Sil.Dbinop (op, de1, de2) ->
           "(" ^ dexp_to_string de1 ^ (Sil.str_binop pe_text op) ^ dexp_to_string de2 ^ ")"
-      | Sil.Dconst (Sil.Cfun pn) ->
+      | Sil.Dconst (Const.Cfun pn) ->
           Procname.to_unique_id pn
       | Sil.Dconst c ->
-          pp_to_string (Sil.pp_const pe_text) c
+          pp_to_string (Const.pp pe_text) c
       | Sil.Dderef de ->
           dexp_to_string de
       | Sil.Dfcall (fun_dexp, args, _, { Sil.cf_virtual = isvirtual })
@@ -169,7 +169,7 @@ let rec typecheck_expr
       (match TypeState.lookup_id id typestate with
        | Some tr -> TypeState.range_add_locs tr [loc]
        | None -> tr_default)
-  | Sil.Const (Sil.Cint i) when IntLit.iszero i ->
+  | Sil.Const (Const.Cint i) when IntLit.iszero i ->
       let (typ, _, locs) = tr_default in
       if PatternMatch.type_is_class typ
       then (typ, TypeAnnotation.const Annotations.Nullable true (TypeOrigin.Const loc), locs)
@@ -302,7 +302,7 @@ let typecheck_instr
     (* Convert a function call to a pvar. *)
     let handle_function_call call_node id =
       match Errdesc.find_normal_variable_funcall call_node id with
-      | Some (Sil.Const (Sil.Cfun pn), _, _, _)
+      | Some (Sil.Const (Const.Cfun pn), _, _, _)
         when not (ComplexExpressions.procname_used_in_condition pn) ->
           begin
             match ComplexExpressions.exp_to_string node' exp with
@@ -509,14 +509,14 @@ let typecheck_instr
             typestate1 in
       check_field_assign ();
       typestate2
-  | Sil.Call ([id], Sil.Const (Sil.Cfun pn), [(_, typ)], loc, _)
+  | Sil.Call ([id], Sil.Const (Const.Cfun pn), [(_, typ)], loc, _)
     when Procname.equal pn ModelBuiltins.__new ||
          Procname.equal pn ModelBuiltins.__new_array ->
       TypeState.add_id
         id
         (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.New, [loc])
         typestate (* new never returns null *)
-  | Sil.Call ([id], Sil.Const (Sil.Cfun pn), (e, typ):: _, loc, _)
+  | Sil.Call ([id], Sil.Const (Const.Cfun pn), (e, typ):: _, loc, _)
     when Procname.equal pn ModelBuiltins.__cast ->
       typecheck_expr_for_errors typestate e loc;
       let e', typestate' =
@@ -525,7 +525,7 @@ let typecheck_instr
       TypeState.add_id id
         (typecheck_expr_simple typestate' e' typ TypeOrigin.ONone loc)
         typestate'
-  | Sil.Call ([id], Sil.Const (Sil.Cfun pn), [(array_exp, t)], loc, _)
+  | Sil.Call ([id], Sil.Const (Const.Cfun pn), [(array_exp, t)], loc, _)
     when Procname.equal pn ModelBuiltins.__get_array_length ->
       let (_, ta, _) = typecheck_expr
           find_canonical_duplicate
@@ -557,11 +557,11 @@ let typecheck_instr
           [loc]
         )
         typestate
-  | Sil.Call (_, Sil.Const (Sil.Cfun pn), _, _, _) when Builtin.is_registered pn ->
+  | Sil.Call (_, Sil.Const (Const.Cfun pn), _, _, _) when Builtin.is_registered pn ->
       typestate (* skip othe builtins *)
   | Sil.Call
       (ret_ids,
-       Sil.Const (Sil.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
+       Sil.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
        etl_,
        loc,
        cflags)
@@ -704,8 +704,8 @@ let typecheck_instr
 
         let handle_negated_condition cond_node =
           let do_instr = function
-            | Sil.Prune (Sil.BinOp (Sil.Eq, _cond_e, Sil.Const (Sil.Cint i)), _, _, _)
-            | Sil.Prune (Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), _cond_e), _, _, _)
+            | Sil.Prune (Sil.BinOp (Sil.Eq, _cond_e, Sil.Const (Const.Cint i)), _, _, _)
+            | Sil.Prune (Sil.BinOp (Sil.Eq, Sil.Const (Const.Cint i), _cond_e), _, _, _)
               when IntLit.iszero i ->
                 let cond_e = Idenv.expand_expr_temps idenv cond_node _cond_e in
                 begin
@@ -740,7 +740,7 @@ let typecheck_instr
                         ()
                     | Some (node', id) ->
                         let () = match Errdesc.find_normal_variable_funcall node' id with
-                          | Some (Sil.Const (Sil.Cfun pn), [e], _, _)
+                          | Some (Sil.Const (Const.Cfun pn), [e], _, _)
                             when ComplexExpressions.procname_optional_isPresent pn ->
                               handle_optional_isPresent node' e
                           | _ -> () in
@@ -770,7 +770,7 @@ let typecheck_instr
               | Some dexp_key, Procname.Java callee_pname_java ->
                   let pname_get =
                     Procname.Java (pname_get_from_pname_put callee_pname_java) in
-                  let dexp_get = Sil.Dconst (Sil.Cfun pname_get) in
+                  let dexp_get = Sil.Dconst (Const.Cfun pname_get) in
                   let dexp_map = Sil.Dpvar pv_map in
                   let args = [dexp_map; dexp_key] in
                   let call_flags = { Sil.cf_default with Sil.cf_virtual = true } in
@@ -871,7 +871,7 @@ let typecheck_instr
           | Sil.Var id ->
               begin
                 match Errdesc.find_normal_variable_funcall node' id with
-                | Some (Sil.Const (Sil.Cfun pn), e1:: _, _, _) when
+                | Some (Sil.Const (Const.Cfun pn), e1:: _, _, _) when
                     filter_callee pn ->
                     Some e1
                 | _ -> None
@@ -905,13 +905,13 @@ let typecheck_instr
             | Some
                 (Sil.Dretcall
                    (Sil.Dconst
-                      (Sil.Cfun (Procname.Java pname_java)), args, loc, call_flags)) ->
+                      (Const.Cfun (Procname.Java pname_java)), args, loc, call_flags)) ->
                 let pname_java' =
                   let object_t = (Some "java.lang", "Object") in
                   Procname.java_replace_return_type
                     (Procname.java_replace_method pname_java "get")
                     object_t in
-                let fun_dexp = Sil.Dconst (Sil.Cfun (Procname.Java pname_java')) in
+                let fun_dexp = Sil.Dconst (Const.Cfun (Procname.Java pname_java')) in
                 Some (Sil.Dretcall (fun_dexp, args, loc, call_flags))
             | _ -> None in
           begin
@@ -944,8 +944,8 @@ let typecheck_instr
           | _ -> typestate2 in
 
         match c with
-        | Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e)
-        | Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
+        | Sil.BinOp (Sil.Eq, Sil.Const (Const.Cint i), e)
+        | Sil.BinOp (Sil.Eq, e, Sil.Const (Const.Cint i)) when IntLit.iszero i ->
             typecheck_expr_for_errors typestate e loc;
             let typestate1, e1, from_call = match from_is_true_on_null e with
               | Some e1 ->
@@ -973,8 +973,8 @@ let typecheck_instr
                   typestate2
             end
 
-        | Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e)
-        | Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
+        | Sil.BinOp (Sil.Ne, Sil.Const (Const.Cint i), e)
+        | Sil.BinOp (Sil.Ne, e, Sil.Const (Const.Cint i)) when IntLit.iszero i ->
             typecheck_expr_for_errors typestate e loc;
             let typestate1, e1, from_call = match from_instanceof e with
               | Some e1 -> (* (e1 instanceof C) implies (e1 != null) *)
@@ -1081,7 +1081,7 @@ let typecheck_node
 
   let typestates_exn = ref [] in
   let handle_exceptions typestate instr = match instr with
-    | Sil.Call (_, Sil.Const (Sil.Cfun callee_pname), _, _, _) ->
+    | Sil.Call (_, Sil.Const (Const.Cfun callee_pname), _, _, _) ->
         let callee_attributes_opt =
           Specs.proc_resolve_attributes callee_pname in
         (* check if the call might throw an exception *)
diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml
index 0fa39eb44..51c8be257 100644
--- a/infer/src/harness/inhabit.ml
+++ b/infer/src/harness/inhabit.ml
@@ -52,7 +52,7 @@ let env_add_instr instr env =
 (** call flags for an allocation or call to a constructor *)
 let cf_alloc = Sil.cf_default
 
-let fun_exp_from_name proc_name = Sil.Const (Sil.Cfun (proc_name))
+let fun_exp_from_name proc_name = Sil.Const (Const.Cfun (proc_name))
 
 let local_name_cntr = ref 0
 
@@ -85,7 +85,7 @@ let rec inhabit_typ typ cfg env =
   with Not_found ->
     let inhabit_internal typ env = match typ with
       | Typ.Tptr (Typ.Tarray (inner_typ, Some _), Typ.Pk_pointer) ->
-          let len = Sil.Const (Sil.Cint (IntLit.one)) in
+          let len = Sil.Const (Const.Cint (IntLit.one)) in
           let arr_typ = Typ.Tarray (inner_typ, Some IntLit.one) in
           inhabit_alloc arr_typ (Some len) typ ModelBuiltins.__new_array env
       | Typ.Tptr (typ, Typ.Pk_pointer) as ptr_to_typ ->
@@ -130,8 +130,8 @@ let rec inhabit_typ typ cfg env =
           let fresh_id = Ident.create_fresh Ident.knormal in
           let read_from_local_instr = Sil.Letderef (fresh_id, fresh_local_exp, ptr_to_typ, env'.pc) in
           (Sil.Var fresh_id, env_add_instr read_from_local_instr env')
-      | Typ.Tint (_) -> (Sil.Const (Sil.Cint (IntLit.zero)), env)
-      | Typ.Tfloat (_) -> (Sil.Const (Sil.Cfloat 0.0), env)
+      | Typ.Tint (_) -> (Sil.Const (Const.Cint (IntLit.zero)), env)
+      | Typ.Tfloat (_) -> (Sil.Const (Const.Cfloat 0.0), env)
       | typ ->
           L.err "Couldn't inhabit typ: %a@." (Typ.pp pe_text) typ;
           assert false in
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index 8158fdef9..8da6bf844 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -169,13 +169,13 @@ let locals_formals program tenv cn impl meth_kind =
 
 let get_constant (c : JBir.const) =
   match c with
-  | `Int i -> Sil.Cint (IntLit.of_int32 i)
-  | `ANull -> Sil.Cint IntLit.null
-  | `Class ot -> Sil.Cclass (Ident.string_to_name (JTransType.object_type_to_string ot))
-  | `Double f -> Sil.Cfloat f
-  | `Float f -> Sil.Cfloat f
-  | `Long i64 -> Sil.Cint (IntLit.of_int64 i64)
-  | `String jstr -> Sil.Cstr (JBasics.jstr_pp jstr)
+  | `Int i -> Const.Cint (IntLit.of_int32 i)
+  | `ANull -> Const.Cint IntLit.null
+  | `Class ot -> Const.Cclass (Ident.string_to_name (JTransType.object_type_to_string ot))
+  | `Double f -> Const.Cfloat f
+  | `Float f -> Const.Cfloat f
+  | `Long i64 -> Const.Cint (IntLit.of_int64 i64)
+  | `String jstr -> Const.Cstr (JBasics.jstr_pp jstr)
 
 let get_binop binop =
   match binop with
@@ -398,10 +398,10 @@ let use_static_final_fields context =
   (not Config.no_static_final) && (JContext.get_meth_kind context) <> JContext.Init
 
 let builtin_new =
-  Sil.Const (Sil.Cfun ModelBuiltins.__new)
+  Sil.Const (Const.Cfun ModelBuiltins.__new)
 
 let builtin_get_array_length =
-  Sil.Const (Sil.Cfun ModelBuiltins.__get_array_length)
+  Sil.Const (Const.Cfun ModelBuiltins.__get_array_length)
 
 let create_sil_deref exp typ loc =
   let no_id = Ident.create_none () in
@@ -463,8 +463,8 @@ let rec expression context pc expr =
               JTransType.sizeof_of_object_type program tenv ot subtypes in
             let builtin =
               (match unop with
-               | JBir.InstanceOf _ -> Sil.Const (Sil.Cfun ModelBuiltins.__instanceof)
-               | JBir.Cast _ -> Sil.Const (Sil.Cfun ModelBuiltins.__cast)
+               | JBir.InstanceOf _ -> Sil.Const (Const.Cfun ModelBuiltins.__instanceof)
+               | JBir.Cast _ -> Sil.Const (Const.Cfun ModelBuiltins.__cast)
                | _ -> assert false) in
             let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.Tvoid)] in
             let ret_id = Ident.create_fresh Ident.knormal in
@@ -594,7 +594,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
     then proc
     else Procname.Java (JTransType.get_method_procname cn' ms method_kind) in
   let call_instrs =
-    let callee_fun = Sil.Const (Sil.Cfun callee_procname) in
+    let callee_fun = Sil.Const (Const.Cfun callee_procname) in
     let return_type =
       match JBasics.ms_rtype ms with
       | None -> Typ.Tvoid
@@ -620,7 +620,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
     | (_, typ) as exp :: _
       when Procname.is_constructor callee_procname && JTransType.is_closeable program tenv typ ->
         let set_file_attr =
-          let set_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__set_file_attribute) in
+          let set_builtin = Sil.Const (Const.Cfun ModelBuiltins.__set_file_attribute) in
           Sil.Call ([], set_builtin, [exp], loc, Sil.cf_default) in
         (* Exceptions thrown in the constructor should prevent adding the resource attribute *)
         call_instrs @ [set_file_attr]
@@ -629,7 +629,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
     | (_, typ) as exp :: []
       when Procname.java_is_close callee_procname && JTransType.is_closeable program tenv typ ->
         let set_mem_attr =
-          let set_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__set_mem_attribute) in
+          let set_builtin = Sil.Const (Const.Cfun ModelBuiltins.__set_mem_attribute) in
           Sil.Call ([], set_builtin, [exp], loc, Sil.cf_default) in
         (* Exceptions thrown in the close method should not prevent the resource from being *)
         (* considered as closed *)
@@ -760,7 +760,7 @@ let is_this expr =
 
 
 let assume_not_null loc sil_expr =
-  let builtin_infer_assume = Sil.Const (Sil.Cfun ModelBuiltins.__infer_assume) in
+  let builtin_infer_assume = Sil.Const (Const.Cfun ModelBuiltins.__infer_assume) in
   let not_null_expr =
     Sil.BinOp (Sil.Ne, sil_expr, Sil.exp_null) in
   let assume_call_flag = { Sil.cf_default with Sil.cf_noreturn = true; } in
@@ -794,7 +794,7 @@ let rec instruction context pc instr : translation =
       JTransType.never_returning_null in
   let trans_monitor_enter_exit context expr pc loc builtin node_desc =
     let instrs, sil_expr, sil_type = expression context pc expr in
-    let builtin_const = Sil.Const (Sil.Cfun builtin) in
+    let builtin_const = Sil.Const (Const.Cfun builtin) in
     let instr = Sil.Call ([], builtin_const, [(sil_expr, sil_type)], loc, Sil.cf_default) in
     let typ_no_ptr = match sil_type with
       | Typ.Tptr (typ, _) -> typ
@@ -897,7 +897,7 @@ let rec instruction context pc instr : translation =
         JContext.add_goto_jump context pc JContext.Exit;
         Instr node
     | JBir.New (var, cn, constr_type_list, constr_arg_list) ->
-        let builtin_new = Sil.Const (Sil.Cfun ModelBuiltins.__new) in
+        let builtin_new = Sil.Const (Const.Cfun ModelBuiltins.__new) in
         let class_type = JTransType.get_class_type program tenv cn in
         let class_type_np = JTransType.get_class_type_no_pointer program tenv cn in
         let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in
@@ -918,7 +918,7 @@ let rec instruction context pc instr : translation =
         Cg.add_edge cg caller_procname constr_procname;
         Instr node
     | JBir.NewArray (var, vt, expr_list) ->
-        let builtin_new_array = Sil.Const (Sil.Cfun ModelBuiltins.__new_array) in
+        let builtin_new_array = Sil.Const (Const.Cfun ModelBuiltins.__new_array) in
         let content_type = JTransType.value_type program tenv vt in
         let array_type = JTransType.create_array_type content_type (IList.length expr_list) in
         let array_name = JContext.set_pvar context var array_type in
@@ -1046,7 +1046,7 @@ let rec instruction context pc instr : translation =
           let sil_assume_in_bound =
             let sil_in_bound =
               let sil_positive_index =
-                Sil.BinOp (Sil.Ge, sil_index_expr, Sil.Const (Sil.Cint IntLit.zero))
+                Sil.BinOp (Sil.Ge, sil_index_expr, Sil.Const (Const.Cint IntLit.zero))
               and sil_less_than_length =
                 Sil.BinOp (Sil.Lt, sil_index_expr, sil_length_expr) in
               Sil.BinOp (Sil.LAnd, sil_positive_index, sil_less_than_length) in
@@ -1059,7 +1059,7 @@ let rec instruction context pc instr : translation =
           let sil_assume_out_of_bound =
             let sil_out_of_bound =
               let sil_negative_index =
-                Sil.BinOp (Sil.Lt, sil_index_expr, Sil.Const (Sil.Cint IntLit.zero))
+                Sil.BinOp (Sil.Lt, sil_index_expr, Sil.Const (Const.Cint IntLit.zero))
               and sil_greater_than_length =
                 Sil.BinOp (Sil.Gt, sil_index_expr, sil_length_expr) in
               Sil.BinOp (Sil.LOr, sil_negative_index, sil_greater_than_length) in
@@ -1090,7 +1090,7 @@ let rec instruction context pc instr : translation =
         and ret_id = Ident.create_fresh Ident.knormal
         and sizeof_expr =
           JTransType.sizeof_of_object_type program tenv object_type Sil.Subtype.subtypes_instof in
-        let check_cast = Sil.Const (Sil.Cfun ModelBuiltins.__instanceof) in
+        let check_cast = Sil.Const (Const.Cfun ModelBuiltins.__instanceof) in
         let args = [(sil_expr, sil_type); (sizeof_expr, Typ.Tvoid)] in
         let call = Sil.Call([ret_id], check_cast, args, loc, Sil.cf_default) in
         let res_ex = Sil.Var ret_id in
diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml
index 1e77f327b..3b64ace1f 100644
--- a/infer/src/java/jTransExn.ml
+++ b/infer/src/java/jTransExn.ml
@@ -41,7 +41,7 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table =
     let id_deactivate = Ident.create_fresh Ident.knormal in
     let instr_deactivate_exn = Sil.Set (Sil.Lvar ret_var, ret_type, Sil.Var id_deactivate, loc) in
     let instr_unwrap_ret_val =
-      let unwrap_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__unwrap_exception) in
+      let unwrap_builtin = Sil.Const (Const.Cfun ModelBuiltins.__unwrap_exception) in
       Sil.Call([id_exn_val], unwrap_builtin, [(Sil.Var id_ret_val, ret_type)], loc, Sil.cf_default) in
     create_node
       loc
@@ -66,7 +66,7 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table =
           | _ -> assert false in
         let id_instanceof = Ident.create_fresh Ident.knormal in
         let instr_call_instanceof =
-          let instanceof_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__instanceof) in
+          let instanceof_builtin = Sil.Const (Const.Cfun ModelBuiltins.__instanceof) in
           let args = [
             (Sil.Var id_exn_val, Typ.Tptr(exn_type, Typ.Pk_pointer));
             (Sil.Sizeof (exn_type, None, Sil.Subtype.exact), Typ.Tvoid)] in
diff --git a/infer/src/java/jTransStaticField.ml b/infer/src/java/jTransStaticField.ml
index 5810f85cd..f12f81178 100644
--- a/infer/src/java/jTransStaticField.ml
+++ b/infer/src/java/jTransStaticField.ml
@@ -185,8 +185,8 @@ let translate_instr_static_field context callee_procdesc fs field_type loc =
   let ret_id = Ident.create_fresh Ident.knormal in
   let caller_procname = (Cfg.Procdesc.get_proc_name caller_procdesc) in
   let callee_procname = Cfg.Procdesc.get_proc_name callee_procdesc in
-  let callee_fun = Sil.Const (Sil.Cfun callee_procname) in
-  let field_arg = Sil.Const (Sil.Cstr (JBasics.fs_name fs)) in
+  let callee_fun = Sil.Const (Const.Cfun callee_procname) in
+  let field_arg = Sil.Const (Const.Cstr (JBasics.fs_name fs)) in
   let call_instr = Sil.Call([ret_id], callee_fun, [field_arg, field_type], loc, Sil.cf_default) in
   Cg.add_edge cg caller_procname callee_procname;
   ([call_instr], Sil.Var ret_id)
diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml
index 893e89bea..0e8c3eebe 100644
--- a/infer/src/llvm/lTrans.ml
+++ b/infer/src/llvm/lTrans.ml
@@ -24,7 +24,7 @@ let ident_of_variable (var : LAst.variable) : Ident.t = (* TODO: use unique stam
 let trans_variable (var : LAst.variable) : Sil.exp = Sil.Var (ident_of_variable var)
 
 let trans_constant : LAst.constant -> Sil.exp = function
-  | Cint i -> Sil.Const (Sil.Cint (IntLit.of_int i))
+  | Cint i -> Sil.Const (Const.Cint (IntLit.of_int i))
   | Cnull -> Sil.exp_null
 
 let trans_operand : LAst.operand -> Sil.exp = function
@@ -97,7 +97,7 @@ let rec trans_annotated_instructions
         | Call (ret_var, func_var, typed_args) ->
             let new_sil_instr = Sil.Call (
                 [ident_of_variable ret_var],
-                Sil.Const (Sil.Cfun (procname_of_function_variable func_var)),
+                Sil.Const (Const.Cfun (procname_of_function_variable func_var)),
                 IList.map (fun (tp, arg) -> (trans_operand arg, trans_typ tp)) typed_args,
                 location, Sil.cf_default) in
             (new_sil_instr :: sil_instrs, locals)
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index df9a6b431..0121548ad 100644
--- a/infer/src/unit/analyzerTester.ml
+++ b/infer/src/unit/analyzerTester.ml
@@ -91,7 +91,7 @@ module StructuredSil = struct
     Cmd (Sil.Set (lhs_exp, rhs_typ, rhs_exp, dummy_loc))
 
   let make_call ?(procname=dummy_procname) ret_ids args =
-    let call_exp = Sil.Const (Sil.Cfun procname) in
+    let call_exp = Sil.Const (Const.Cfun procname) in
     Cmd (Sil.Call (ret_ids, call_exp, args, dummy_loc, Sil.cf_default))
 
   let id_assign_id ?(rhs_typ=dummy_typ) lhs rhs =