diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re
index 1f8e2bd1f..e99fe8995 100644
--- a/infer/src/IR/Sil.re
+++ b/infer/src/IR/Sil.re
@@ -657,7 +657,7 @@ type dexp =
   | Darray of dexp dexp
   | Dbinop of binop dexp dexp
   | Dconst of const
-  | Dsizeof of typ Subtype.t
+  | Dsizeof of typ (option exp) Subtype.t
   | Dderef of dexp
   | Dfcall of dexp (list dexp) Location.t call_flags
   | Darrow of dexp Ident.fieldname
@@ -769,8 +769,10 @@ and exp =
   | Lfield of exp Ident.fieldname typ
   /** An array index offset: [exp1\[exp2\]] */
   | Lindex of exp exp
-  /** A sizeof expression */
-  | Sizeof of typ Subtype.t;
+  /** A sizeof expression. [Sizeof typ (Some len)] represents the size of a value of type [typ]
+      which ends in an extensible array of length [len].  The lengths in [Tarray] record the
+      statically determined lengths, while the lengths in [Sizeof] record the dynamic lengths. */
+  | Sizeof of typ (option exp) Subtype.t;
 
 
 /** Kind of prune instruction */
@@ -937,7 +939,7 @@ let is_objc_ref_counter_field (fld, _, a) =>
 
 let has_objc_ref_counter hpred =>
   switch hpred {
-  | Hpointsto _ _ (Sizeof (Tstruct struct_typ) _) =>
+  | Hpointsto _ _ (Sizeof (Tstruct struct_typ) _ _) =>
     IList.exists is_objc_ref_counter_field struct_typ.instance_fields
   | _ => false
   };
@@ -1642,12 +1644,17 @@ and exp_compare (e1: exp) (e2: exp) :int =>
     }
   | (Lindex _, _) => (-1)
   | (_, Lindex _) => 1
-  | (Sizeof t1 s1, Sizeof t2 s2) =>
+  | (Sizeof t1 l1 s1, Sizeof t2 l2 s2) =>
     let n = typ_compare t1 t2;
     if (n != 0) {
       n
     } else {
-      Subtype.compare s1 s2
+      let n = opt_compare exp_compare l1 l2;
+      if (n != 0) {
+        n
+      } else {
+        Subtype.compare s1 s2
+      }
     }
   };
 
@@ -2190,7 +2197,7 @@ let rec dexp_to_string =
       ampersand ^ s
     }
   | Dunop op de => str_unop op ^ dexp_to_string de
-  | Dsizeof typ _ => pp_to_string (pp_typ_full pe_text) typ
+  | Dsizeof typ _ _ => pp_to_string (pp_typ_full pe_text) typ
   | Dunknown => "unknown"
   | Dretcall de _ _ _ => "returned by " ^ dexp_to_string de
 /** Pretty print a dexp. */
@@ -2397,7 +2404,9 @@ and _pp_exp pe0 pp_t f e0 => {
     | Lvar pv => Pvar.pp pe f pv
     | Lfield e fld _ => F.fprintf f "%a.%a" pp_exp e Ident.pp_fieldname fld
     | Lindex e1 e2 => F.fprintf f "%a[%a]" pp_exp e1 pp_exp e2
-    | Sizeof t s => F.fprintf f "sizeof(%a%a)" pp_t t Subtype.pp s
+    | Sizeof t l s =>
+      let pp_len f l => Option.map_default (F.fprintf f "[%a]" pp_exp) () l;
+      F.fprintf f "sizeof(%a%a%a)" pp_t t pp_len l Subtype.pp s
     }
   };
   color_post_wrapper changed pe0 f
@@ -2434,14 +2443,20 @@ let d_exp_list (el: list exp) => L.add_print_action (L.PTexp_list, Obj.repr el);
 
 let pp_texp pe f =>
   fun
-  | Sizeof t s => F.fprintf f "%a%a" (pp_typ pe) t Subtype.pp s
+  | Sizeof t l s => {
+      let pp_len f l => Option.map_default (F.fprintf f "[%a]" (pp_exp pe)) () l;
+      F.fprintf f "%a%a%a" (pp_typ pe) t pp_len l Subtype.pp s
+    }
   | e => (pp_exp pe) f e;
 
 
 /** Pretty print a type with all the details. */
 let pp_texp_full pe f =>
   fun
-  | Sizeof t s => F.fprintf f "%a%a" (pp_typ_full pe) t Subtype.pp s
+  | Sizeof t l s => {
+      let pp_len f l => Option.map_default (F.fprintf f "[%a]" (pp_exp pe)) () l;
+      F.fprintf f "%a%a%a" (pp_typ_full pe) t pp_len l Subtype.pp s
+    }
   | e => (_pp_exp pe) (pp_typ_full pe) f e;
 
 
@@ -3290,7 +3305,7 @@ let unsome_typ s =>
     If not a sizeof, return the default type if given, otherwise raise an exception */
 let texp_to_typ default_opt =>
   fun
-  | Sizeof t _ => t
+  | Sizeof t _ _ => t
   | _ => unsome_typ "texp_to_typ" default_opt;
 
 
@@ -3416,7 +3431,10 @@ let rec exp_fpv =
   | Lvar name => [name]
   | Lfield e _ _ => exp_fpv e
   | Lindex e1 e2 => exp_fpv e1 @ exp_fpv e2
-  | Sizeof _ => []
+  /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
+  /* | Sizeof _ None _ => [] */
+  /* | Sizeof _ (Some l) _ => exp_fpv l */
+  | Sizeof _ _ _ => []
 and exp_list_fpv el => IList.flatten (IList.map exp_fpv el);
 
 let atom_fpv =
@@ -3611,7 +3629,10 @@ let rec exp_fav_add fav =>
       exp_fav_add fav e1;
       exp_fav_add fav e2
     }
-  | Sizeof _ => ();
+  /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
+  /* | Sizeof _ None _ => () */
+  /* | Sizeof _ (Some l) _ => exp_fav_add fav l; */
+  | Sizeof _ _ _ => ();
 
 let exp_fav = fav_imperative_to_functional exp_fav_add;
 
@@ -4051,7 +4072,7 @@ and exp_sub (subst: subst) e =>
     let e1' = exp_sub subst e1;
     let e2' = exp_sub subst e2;
     Lindex e1' e2'
-  | Sizeof t s => Sizeof (typ_sub subst t) s
+  | Sizeof t l s => Sizeof (typ_sub subst t) (Option.map (exp_sub subst) l) s
   };
 
 let instr_sub (subst: subst) instr => {
@@ -4599,8 +4620,11 @@ let exp_get_vars exp => {
         (fun vars_acc (captured_exp, _, _) => exp_get_vars_ captured_exp vars_acc)
         vars
         captured_vars
-    | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _)
-    | Sizeof _ => vars
+    | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _) => vars
+    /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
+    /* | Sizeof _ None _ => vars */
+    /* | Sizeof _ (Some l) _ => exp_get_vars_ l vars */
+    | Sizeof _ _ _ => vars
     };
   exp_get_vars_ exp ([], [])
 };
@@ -4615,7 +4639,8 @@ let exp_get_offsets exp => {
     | UnOp _
     | BinOp _
     | Lvar _
-    | Sizeof _ => offlist_past
+    | Sizeof _ None _ => offlist_past
+    | Sizeof _ (Some l) _ => f offlist_past l
     | Cast _ sub_exp => f offlist_past sub_exp
     | Lfield sub_exp fldname typ => f [Off_fld fldname typ, ...offlist_past] sub_exp
     | Lindex sub_exp e => f [Off_index e, ...offlist_past] sub_exp
diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei
index ea00a4b45..c4ec13d71 100644
--- a/infer/src/IR/Sil.rei
+++ b/infer/src/IR/Sil.rei
@@ -230,7 +230,7 @@ type dexp =
   | Darray of dexp dexp
   | Dbinop of binop dexp dexp
   | Dconst of const
-  | Dsizeof of typ Subtype.t
+  | Dsizeof of typ (option exp) Subtype.t
   | Dderef of dexp
   | Dfcall of dexp (list dexp) Location.t call_flags
   | Darrow of dexp Ident.fieldname
@@ -343,7 +343,7 @@ and exp =
   /** An array index offset: [exp1\[exp2\]] */
   | Lindex of exp exp
   /** A sizeof expression */
-  | Sizeof of typ Subtype.t;
+  | Sizeof of typ (option exp) Subtype.t;
 
 let struct_typ_equal: struct_typ => struct_typ => bool;
 
@@ -539,7 +539,7 @@ type strexp =
 and hpred =
   | Hpointsto of exp strexp exp
   /** represents [exp|->strexp:typexp] where [typexp]
-      is an expression representing a type, e.h. [sizeof(t)]. */
+      is an expression representing a type, e.g. [sizeof(t)]. */
   | Hlseg of lseg_kind hpara exp exp (list exp)
   /** higher - order predicate for singly - linked lists.
       Should ensure that exp1!= exp2 implies that exp1 is allocated.
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index dee8f48eb..a1af433cc 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -420,7 +420,7 @@ let typ_get_recursive_flds tenv typ_exp =
         false
   in
   match typ_exp with
-  | Sil.Sizeof (typ, _) ->
+  | Sil.Sizeof (typ, _, _) ->
       (match Tenv.expand_type tenv typ with
        | Sil.Tint _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ | Sil.Tfloat _ -> []
        | Sil.Tstruct { Sil.instance_fields } ->
@@ -903,14 +903,14 @@ let get_cycle root prop =
           let visited' = (fst et_src):: visited in
           let res = (match get_points_to e with
               | None -> path, false
-              | Some (Sil.Hpointsto(_, Sil.Estruct(fl, _), Sil.Sizeof(te, _))) ->
+              | Some (Sil.Hpointsto(_, Sil.Estruct(fl, _), Sil.Sizeof(te, _, _))) ->
                   dfs e_root (e, te) ((et_src, f, e):: path) fl visited'
               | _ -> path, false (* check for lists *)) in
           if snd res then res
           else dfs e_root et_src path el' visited') in
   L.d_strln "Looking for cycle with root expression: "; Sil.d_hpred root; L.d_strln "";
   match root with
-  | Sil.Hpointsto(e_root, Sil.Estruct(fl, _), Sil.Sizeof(te, _)) ->
+  | Sil.Hpointsto(e_root, Sil.Estruct(fl, _), Sil.Sizeof(te, _, _)) ->
       let se_root = Sil.Eexp(e_root, Sil.Inone) in
       (* start dfs with empty path and expr pointing to root *)
       let (pot_cycle, res) = dfs se_root (se_root, te) [] fl [] in
@@ -929,7 +929,7 @@ let get_cycle root prop =
 let should_raise_objc_leak hpred =
   match hpred with
   | Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Sil.Const (Sil.Cint i)), _)):: _, _),
-                  Sil.Sizeof (typ, _))
+                  Sil.Sizeof (typ, _, _))
     when Ident.fieldname_is_hidden fn && Sil.Int.gt i Sil.Int.zero (* counter > 0 *) ->
       Mleak_buckets.should_raise_objc_leak typ
   | _ -> None
@@ -949,7 +949,7 @@ let get_var_retain_cycle _prop =
     | _ -> false in
   let is_hpred_block v h =
     match h, v with
-    | Sil.Hpointsto (e, _, Sil.Sizeof(typ, _)), Sil.Eexp (e', _)
+    | Sil.Hpointsto (e, _, Sil.Sizeof(typ, _, _)), Sil.Eexp (e', _)
       when Sil.exp_equal e e' && Sil.is_block_type typ -> true
     | _, _ -> false in
   let find v =
@@ -967,7 +967,7 @@ let get_var_retain_cycle _prop =
     | Some pvar -> [((sexp pvar, t), f, e')]
     | _ -> (match find_block e with
         | Some blk -> [((sexp blk, t), f, e')]
-        | _ -> [((sexp (Sil.Sizeof(t, Sil.Subtype.exact)), t), f, e')]) in
+        | _ -> [((sexp (Sil.Sizeof (t, None, Sil.Subtype.exact)), t), f, e')]) in
   (* returns the pvars of the first cycle we find in sigma. *)
   (* This is an heuristic that works if there is one cycle. *)
   (* In case there are more than one cycle we may return not necessarily*)
diff --git a/infer/src/backend/autounit.ml b/infer/src/backend/autounit.ml
index 068c90849..7fb99f361 100644
--- a/infer/src/backend/autounit.ml
+++ b/infer/src/backend/autounit.ml
@@ -332,7 +332,7 @@ let create_idmap sigma : idmap =
         extend_idmap id { typ = t; alloc = true } idmap
     | _ -> () in
   let do_hpred = function
-    | Sil.Hpointsto (e, se, Sil.Sizeof (typ, _)) ->
+    | Sil.Hpointsto (e, se, Sil.Sizeof (typ, _, _)) ->
         do_lhs_e e (Sil.Tptr (typ, Sil.Pk_pointer));
         do_se se typ
     | Sil.Hlseg (_, _, e, f, el) ->
@@ -427,7 +427,7 @@ let pp_texp_for_malloc fmt =
     | Sil.Tarray (t, e) ->
         Sil.Tarray (handle_arr_size t, e) in
   function
-  | Sil.Sizeof (typ, _) ->
+  | Sil.Sizeof (typ, _, _) ->
       let typ' = handle_arr_size typ in
       F.fprintf fmt "sizeof(%a)" (pp_typ_c pe) typ'
   | e -> pp_exp_c pe fmt e
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index 18a0c3094..c4d9f300f 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -821,8 +821,10 @@ let rec exp_construct_fresh side e =
       let e1' = exp_construct_fresh side e1 in
       let e2' = exp_construct_fresh side e2 in
       Sil.Lindex(e1', e2')
-  | Sil.Sizeof _ ->
+  | Sil.Sizeof (_, None, _) ->
       e
+  | Sil.Sizeof (typ, Some len, st) ->
+      Sil.Sizeof (typ, Some (exp_construct_fresh side len), st)
 
 let strexp_construct_fresh side =
   let f (e, inst_opt) = (exp_construct_fresh side e, inst_opt) in
@@ -948,12 +950,18 @@ let rec exp_partial_join (e1: Sil.exp) (e2: Sil.exp) : Sil.exp =
       let e1'' = exp_partial_join e1 e2 in
       let e2'' = exp_partial_join e1' e2' in
       Sil.Lindex(e1'', e2'')
-  | Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) ->
-      Sil.Sizeof (typ_partial_join t1 t2, Sil.Subtype.join st1 st2)
+  | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, len2, st2) ->
+      Sil.Sizeof (typ_partial_join t1 t2, len_partial_join len1 len2, Sil.Subtype.join st1 st2)
   | _ ->
       L.d_str "exp_partial_join no match "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln ();
       raise IList.Fail
 
+and len_partial_join len1 len2 =
+  match len1, len2 with
+  | None, _ -> len2
+  | _, None -> len1
+  | Some len1, Some len2 -> Some (size_partial_join len1 len2)
+
 and size_partial_join size1 size2 = match size1, size2 with
   | Sil.BinOp(Sil.PlusA, e1, Sil.Const c1), Sil.BinOp(Sil.PlusA, e2, Sil.Const c2) ->
       let e' = exp_partial_join e1 e2 in
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index 815ddf587..3e45a9bb3 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -294,7 +294,7 @@ let rec dotty_mk_node pe sigma =
   let n = !dotty_state_count in
   incr dotty_state_count;
   let do_hpred_lambda exp_color = function
-    | (Sil.Hpointsto (e, Sil.Earray(e', l, _), Sil.Sizeof(Sil.Tarray(t, _), _)), lambda) ->
+    | (Sil.Hpointsto (e, Sil.Earray (e', l, _), Sil.Sizeof (Sil.Tarray(t, _), _, _)), lambda) ->
         incr dotty_state_count;  (* increment once more n+1 is the box for the array *)
         let e_color_str = color_to_str (exp_color e) in
         let e_color_str'= color_to_str (exp_color e') in
@@ -673,7 +673,7 @@ let filter_useless_spec_dollar_box (nodes: dotty_node list) (links: link list) =
 (* print a struct node *)
 let rec print_struct f pe e te l coo c =
   let print_type = match te with
-    | Sil.Sizeof (t, _) ->
+    | Sil.Sizeof (t, _, _) ->
         let str_t = Sil.typ_to_string t in
         (match Str.split_delim (Str.regexp_string Config.anonymous_block_prefix) str_t with
          | [_; _] -> "BLOCK object"
diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml
index 46387ceb3..71a820971 100644
--- a/infer/src/backend/errdesc.ml
+++ b/infer/src/backend/errdesc.ml
@@ -388,9 +388,9 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
     | Sil.Cast (_, e1) ->
         if verbose then (L.d_str "exp_rv_dexp: Cast "; Sil.d_exp e; L.d_ln ());
         _exp_rv_dexp seen node e1
-    | Sil.Sizeof (typ, sub) ->
+    | Sil.Sizeof (typ, len, sub) ->
         if verbose then (L.d_str "exp_rv_dexp: type "; Sil.d_exp e; L.d_ln ());
-        Some (Sil.Dsizeof (typ, sub))
+        Some (Sil.Dsizeof (typ, len, sub))
     | _ ->
         if verbose then (L.d_str "exp_rv_dexp: no match for  "; Sil.d_exp e; L.d_ln ());
         None
@@ -497,12 +497,12 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
     (Pvar.is_local pvar || Pvar.is_global pvar) &&
     not (pvar_is_frontend_tmp pvar) &&
     match hpred_typ_opt, find_typ_without_ptr prop pvar with
-    | Some (Sil.Sizeof (t1, _)), Some (Sil.Sizeof (Sil.Tptr (_t2, _), _)) ->
+    | Some (Sil.Sizeof (t1, _, _)), Some (Sil.Sizeof (Sil.Tptr (t2_, _), _, _)) ->
         (try
-           let t2 = Tenv.expand_type tenv _t2 in
+           let t2 = Tenv.expand_type tenv t2_ in
            Sil.typ_equal t1 t2
          with exn when SymOp.exn_not_failure exn -> false)
-    | Some (Sil.Sizeof (Sil.Tint _, _)), Some (Sil.Sizeof (Sil.Tint _, _))
+    | Some (Sil.Sizeof (Sil.Tint _, _, _)), Some (Sil.Sizeof (Sil.Tint _, _, _))
       when is_file -> (* must be a file opened with "open" *)
         true
     | _ -> false in
@@ -570,7 +570,7 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option =
           (match lexp with
            | Sil.Lvar pv ->
                let typo = match texp with
-                 | Sil.Sizeof (Sil.Tstruct struct_typ, _) ->
+                 | Sil.Sizeof (Sil.Tstruct struct_typ, _, _) ->
                      (try
                         let _, t, _ =
                           IList.find (fun (f', _, _) ->
@@ -596,7 +596,7 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option =
           (match lexp with
            | Sil.Lvar pv when not (pvar_is_frontend_tmp pv) ->
                let typo = match texp with
-                 | Sil.Sizeof (typ, _) -> Some typ
+                 | Sil.Sizeof (typ, _, _) -> Some typ
                  | _ -> None in
                Some (Sil.Dpvar pv), typo
            | Sil.Var id ->
diff --git a/infer/src/backend/iList.ml b/infer/src/backend/iList.ml
index 1a3a1b90a..c9b8e8bc9 100644
--- a/infer/src/backend/iList.ml
+++ b/infer/src/backend/iList.ml
@@ -28,6 +28,11 @@ let sort = List.sort
 let stable_sort = List.stable_sort
 let tl = List.tl
 
+let rec last = function
+  | [] -> invalid_arg "IList.last"
+  | [x] -> x
+  | _ :: xs -> last xs
+
 (** tail-recursive variant of List.fold_right *)
 let fold_right f l a =
   let g x y = f y x in
diff --git a/infer/src/backend/iList.mli b/infer/src/backend/iList.mli
index 255cbfd16..c2a241d75 100644
--- a/infer/src/backend/iList.mli
+++ b/infer/src/backend/iList.mli
@@ -64,6 +64,9 @@ val split : ('a * 'b) list -> 'a list * 'b list
 val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list
 val tl : 'a list -> 'a list
 
+(** last element, raises invalid_arg if empty *)
+val last : 'a list -> 'a
+
 (* Drops the first n elements from a list. *)
 val drop_first : int -> 'a list -> 'a list
 
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 62dd790db..e1b53e106 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -640,7 +640,7 @@ let report_context_leaks pname sigma tenv =
   let context_exps =
     IList.fold_left
       (fun exps hpred -> match hpred with
-         | Sil.Hpointsto (_, Eexp (exp, _), Sizeof (Tptr (Tstruct struct_typ, _), _))
+         | Sil.Hpointsto (_, Eexp (exp, _), Sizeof (Tptr (Tstruct struct_typ, _), _, _))
            when AndroidFramework.is_context tenv struct_typ &&
                 not (AndroidFramework.is_application tenv struct_typ) ->
              (exp, struct_typ) :: exps
@@ -807,8 +807,8 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr
   let sigma_new_formals =
     let do_formal (pv, typ) =
       let texp = match !Config.curr_language with
-        | Config.Clang -> Sil.Sizeof (typ, Sil.Subtype.exact)
-        | Config.Java -> Sil.Sizeof (typ, Sil.Subtype.subtypes) in
+        | Config.Clang -> Sil.Sizeof (typ, None, Sil.Subtype.exact)
+        | Config.Java -> Sil.Sizeof (typ, None, Sil.Subtype.subtypes) in
       Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_formal (pv, texp, None) in
     IList.map do_formal new_formals in
   let sigma_seed =
diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml
index ee99d596a..0b7a7b53f 100644
--- a/infer/src/backend/localise.ml
+++ b/infer/src/backend/localise.ml
@@ -687,7 +687,7 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
       | Some (Sil.Sizeof (Sil.Tstruct
                             { Sil.csu = Csu.Class _;
                               Sil.struct_name = Some classname;
-                            }, _)) ->
+                            }, _, _)) ->
           " of type " ^ Mangled.to_string classname ^ " "
       | _ -> " " in
     let desc_str =
@@ -772,7 +772,7 @@ let desc_retain_cycle prop cycle loc cycle_dotty =
           else e_str in
         str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") object "^e_str^" retaining "^e_str^"."^(Ident.fieldname_to_string f)^", ";
         ct:=!ct +1
-    | Sil.Eexp(Sil.Sizeof(typ, _), _) ->
+    | Sil.Eexp (Sil.Sizeof (typ, _, _), _) ->
         str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") an object of "^(Sil.typ_to_string typ)^" retaining another object via instance variable "^(Ident.fieldname_to_string f)^", ";
         ct:=!ct +1
     | _ -> () in
diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml
index 75c43d3ce..55bc82eac 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/modelBuiltins.ml
@@ -76,7 +76,8 @@ let add_array_to_prop pdesc prop_ lexp typ =
           let size = Sil.Var(Ident.create_fresh Ident.kfootprint) in
           let s = mk_empty_array_rearranged size in
           let hpred =
-            Prop.mk_ptsto n_lexp s (Sil.Sizeof(Sil.Tarray(typ', size), Sil.Subtype.exact)) in
+            Prop.mk_ptsto n_lexp s
+              (Sil.Sizeof (Sil.Tarray (typ', size), None, Sil.Subtype.exact)) in
           let sigma = Prop.get_sigma prop in
           let sigma_fp = Prop.get_sigma_footprint prop in
           let prop'= Prop.replace_sigma (hpred:: sigma) prop in
@@ -157,13 +158,13 @@ let create_type tenv n_lexp typ prop =
         | Sil.Tptr (typ', _) ->
             let sexp = Sil.Estruct ([], Sil.inst_none) in
             let typ'' = Tenv.expand_type tenv typ' in
-            let texp = Sil.Sizeof (typ'', Sil.Subtype.subtypes) in
+            let texp = Sil.Sizeof (typ'', None, Sil.Subtype.subtypes) in
             let hpred = Prop.mk_ptsto n_lexp sexp texp in
             Some hpred
         | Sil.Tarray _ ->
             let size = Sil.Var(Ident.create_fresh Ident.kfootprint) in
             let sexp = mk_empty_array size in
-            let texp = Sil.Sizeof (typ, Sil.Subtype.subtypes) in
+            let texp = Sil.Sizeof (typ, None, Sil.Subtype.subtypes) in
             let hpred = Prop.mk_ptsto n_lexp sexp texp in
             Some hpred
         | _ -> None in
@@ -569,7 +570,7 @@ let execute___release_autorelease_pool
                  | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 exp
                  | _ -> false) (Prop.get_sigma prop_) in
              match hpred with
-             | Sil.Hpointsto(_, _, Sil.Sizeof (typ, _)) ->
+             | Sil.Hpointsto (_, _, Sil.Sizeof (typ, _, _)) ->
                  let res1 =
                    execute___objc_release
                      { builtin_args with
@@ -668,7 +669,7 @@ let execute___objc_cast { Builtin.pdesc; prop_; path; ret_ids; args; }
              | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 val1
              | _ -> false) (Prop.get_sigma prop) in
          match hpred, texp2 with
-         | Sil.Hpointsto(val1, _, _), Sil.Sizeof (_, _) ->
+         | Sil.Hpointsto (val1, _, _), Sil.Sizeof _ ->
              let prop' = replace_ptsto_texp prop val1 texp2 in
              [(return_result val1 prop' ret_ids, path)]
          | _ -> [(return_result val1 prop ret_ids, path)]
@@ -760,19 +761,22 @@ let execute_alloc mk can_return_null
     | Sil.BinOp (bop, e1', e2') ->
         Sil.BinOp (bop, evaluate_char_sizeof e1', evaluate_char_sizeof e2')
     | Sil.Const _ | Sil.Cast _ | Sil.Lvar _ | Sil.Lfield _ | Sil.Lindex _ -> e
-    | Sil.Sizeof (Sil.Tarray(Sil.Tint ik, size), _) when Sil.ikind_is_char ik ->
-        evaluate_char_sizeof size
+    | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, _), Some len, _) when Sil.ikind_is_char ik ->
+        evaluate_char_sizeof len
+    | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, len), None, _) when Sil.ikind_is_char ik ->
+        evaluate_char_sizeof len
     | Sil.Sizeof _ -> e in
-  let handle_sizeof_exp size_exp =
-    Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, size_exp), Sil.Subtype.exact) in
+  let handle_sizeof_exp len =
+    Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, len), Some len, Sil.Subtype.exact) in
   let size_exp, procname = match args with
-    | [(Sil.Sizeof (Sil.Tstruct
-                      { Sil.csu = Csu.Class Csu.Objc; struct_name = Some c } as s, subt), _)] ->
+    | [(Sil.Sizeof
+          (Sil.Tstruct
+             { Sil.csu = Csu.Class Csu.Objc; struct_name = Some c } as s, len, subt), _)] ->
         let struct_type =
           match AttributesTable.get_correct_type_from_objc_class_name c with
           | Some struct_type -> struct_type
           | None -> s in
-        Sil.Sizeof (struct_type, subt), pname
+        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), _)] ->
@@ -822,7 +826,7 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r)
                    | Sil.Hpointsto (e, _, _) -> Sil.exp_equal e n_lexp
                    | _ -> false) (Prop.get_sigma prop) in
                match hpred with
-               | Sil.Hpointsto (_, _, Sil.Sizeof (dynamic_type, _)) -> dynamic_type
+               | Sil.Hpointsto (_, _, Sil.Sizeof (dynamic_type, _, _)) -> dynamic_type
                | _ -> typ
              with Not_found -> typ in
            let typ_string = Sil.typ_to_string typ in
@@ -1157,7 +1161,7 @@ let execute_objc_alloc_no_fail
     { Builtin.pdesc; tenv; ret_ids; loc; } =
   let alloc_fun = Sil.Const (Sil.Cfun __objc_alloc_no_fail) in
   let ptr_typ = Sil.Tptr (typ, Sil.Pk_pointer) in
-  let sizeof_typ = Sil.Sizeof (typ, Sil.Subtype.exact) 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), Sil.Tvoid]
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index 424269bb9..21e352862 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -456,9 +456,10 @@ let sym_eval abs e =
         Sil.Const (Sil.Cclosure { c with captured_vars; })
     | Sil.Const _ ->
         e
-    | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, e), _)
+    | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, l), None, _)
+    | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, _), Some l, _)
       when Sil.ikind_is_char ik && !Config.curr_language <> Config.Java ->
-        eval e
+        eval l
     | Sil.Sizeof _ ->
         e
     | Sil.Cast (_, e1) ->
@@ -593,7 +594,7 @@ let sym_eval abs e =
         eval (Sil.BinOp (Sil.PlusPI, e11, e2'))
     | Sil.BinOp
         (Sil.PlusA,
-         (Sil.Sizeof (Sil.Tstruct struct_typ, _) as e1),
+         (Sil.Sizeof (Sil.Tstruct struct_typ, None, _) as e1),
          e2) ->
         (* pattern for extensible structs given a struct declatead as struct s { ... t arr[n] ... },
            allocation pattern malloc(sizeof(struct s) + k * siezof(t)) turn it into
@@ -603,13 +604,13 @@ let sym_eval abs e =
         let instance_fields = struct_typ.Sil.instance_fields in
         (match IList.rev instance_fields, e2' with
            (fname, Sil.Tarray (typ, size), _) :: ltfa,
-           Sil.BinOp(Sil.Mult, num_elem, Sil.Sizeof (texp, st))
+           Sil.BinOp(Sil.Mult, num_elem, Sil.Sizeof (texp, None, st))
            when instance_fields != [] && Sil.typ_equal typ texp ->
              let size' = Sil.BinOp(Sil.PlusA, size, num_elem) in
              let ltfa' = (fname, Sil.Tarray(typ, size'), Sil.item_annotation_empty) :: ltfa in
              let struct_typ' =
                { struct_typ with Sil.instance_fields = IList.rev ltfa' } in
-             Sil.Sizeof (Sil.Tstruct struct_typ', st)
+             Sil.Sizeof (Sil.Tstruct struct_typ', None, st)
          | _ -> Sil.BinOp(Sil.PlusA, e1', e2'))
     | Sil.BinOp (Sil.PlusA as oplus, e1, e2)
     | Sil.BinOp (Sil.PlusPI as oplus, e1, e2) ->
@@ -625,6 +626,19 @@ let sym_eval abs e =
           | _ -> Sil.BinOp (ominus, x, y) in
         begin
           match e1', e2' with
+          | Sil.Sizeof (typ, Some len1, st),
+            Sil.BinOp (Sil.Mult, len2, Sil.Sizeof (elt, None, _))
+            when isPlusA
+              && (match typ with
+                  | Sil.Tarray (elt2, _) ->
+                      Sil.typ_equal elt elt2
+                  | Sil.Tstruct {instance_fields= _::_ as flds} ->
+                      Sil.typ_equal elt (snd3 (IList.last flds))
+                  | _ ->
+                      false) ->
+              (* pattern for extensible structs:
+                 sizeof(struct s {... t[l]}) + k * sizeof(elt)) = sizeof(struct s {... t[l + k]}) *)
+              Sil.Sizeof (typ, Some (len1 +++ len2), st)
           | Sil.Const c, _ when iszero_int_float c ->
               e2'
           | _, Sil.Const c when iszero_int_float c ->
@@ -691,13 +705,6 @@ let sym_eval abs e =
     | Sil.BinOp (Sil.MinusPP, e1, e2) ->
         if abs then Sil.exp_get_undefined false
         else Sil.BinOp (Sil.MinusPP, eval e1, eval e2)
-    | Sil.BinOp (Sil.Mult, esize, Sil.Sizeof (t, st))
-    | Sil.BinOp(Sil.Mult, Sil.Sizeof (t, st), esize) ->
-        begin
-          match eval esize, eval (Sil.Sizeof (t, st)) with
-          | Sil.Const (Sil.Cint i), e' when Sil.Int.isone i -> e'
-          | esize', e' -> Sil.BinOp(Sil.Mult, esize', e')
-        end
     | Sil.BinOp (Sil.Mult, e1, e2) ->
         let e1' = eval e1 in
         let e2' = eval e2 in
@@ -721,6 +728,9 @@ let sym_eval abs e =
               Sil.exp_float (v *. w)
           | Sil.Var _, Sil.Var _ ->
               Sil.BinOp(Sil.Mult, e1', e2')
+          | _, Sil.Sizeof _
+          | Sil.Sizeof _, _ ->
+              Sil.BinOp(Sil.Mult, e1', e2')
           | _, _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp(Sil.Mult, e1', e2')
         end
@@ -739,10 +749,11 @@ let sym_eval abs e =
               Sil.exp_int (Sil.Int.div n m)
           | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
               Sil.exp_float (v /.w)
-          | Sil.Sizeof(Sil.Tarray(typ, size), _), Sil.Sizeof(_typ, _)
-            (* pattern: sizeof(arr) / sizeof(arr[0]) = size of arr *)
-            when Sil.typ_equal _typ typ ->
-              size
+          | Sil.Sizeof (Sil.Tarray (elt, _), Some len, _), Sil.Sizeof (elt2, None, _)
+          | Sil.Sizeof (Sil.Tarray (elt, len), None, _), Sil.Sizeof (elt2, None, _)
+            (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
+            when Sil.typ_equal elt elt2 ->
+              len
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.Div, e1', e2')
         end
@@ -842,7 +853,8 @@ let exp_normalize sub exp =
   else sym_eval false exp'
 
 let rec texp_normalize sub exp = match exp with
-  | Sil.Sizeof (typ, st) -> Sil.Sizeof (typ_normalize sub typ, st)
+  | Sil.Sizeof (typ, len, st) ->
+      Sil.Sizeof (typ_normalize sub typ, Option.map (exp_normalize sub) len, st)
   | _ -> exp_normalize sub exp
 
 (* NOTE: usage of == operator in flds_norm and typ_normalize is intended*)
@@ -1141,7 +1153,7 @@ let rec strexp_normalize sub se =
       end
 
 (** create a strexp of the given type, populating the structures if [expand_structs] is true *)
-let rec create_strexp_of_type tenvo struct_init_mode typ inst =
+let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
   let init_value () =
     let create_fresh_var () =
       let fresh_id =
@@ -1154,24 +1166,30 @@ let rec create_strexp_of_type tenvo struct_init_mode typ inst =
       | _ -> Sil.exp_zero
     else
       create_fresh_var () in
-  match typ with
-  | Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ ->
+  match typ, len with
+  | (Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _), None ->
       Sil.Eexp (init_value (), inst)
-  | Sil.Tstruct { Sil.instance_fields } ->
-      begin
-        match struct_init_mode with
-        | No_init -> Sil.Estruct ([], inst)
-        | Fld_init ->
-            let f (fld, t, a) =
-              if Sil.is_objc_ref_counter_field (fld, t, a) then
-                (fld, Sil.Eexp (Sil.exp_one, inst))
-              else
-                (fld, create_strexp_of_type tenvo struct_init_mode t inst) in
-            Sil.Estruct (IList.map f instance_fields, inst)
-      end
-  | Sil.Tarray (_, size) ->
+  | Sil.Tstruct { Sil.instance_fields }, _ -> (
+      match struct_init_mode with
+      | No_init ->
+          Sil.Estruct ([], inst)
+      | Fld_init ->
+          (* pass len as an accumulator, so that it is passed to create_strexp_of_type for the last
+             field, but always return None so that only the last field receives len *)
+          let f (fld, t, a) (flds, len) =
+            if Sil.is_objc_ref_counter_field (fld, t, a) then
+              ((fld, Sil.Eexp (Sil.exp_one, inst)) :: flds, None)
+            else
+              ((fld, create_strexp_of_type tenvo struct_init_mode t len inst) :: flds, None) in
+          let flds, _ = IList.fold_right f instance_fields ([], len) in
+          Sil.Estruct (flds, inst)
+    )
+  | Sil.Tarray (_, size), None ->
       Sil.Earray (size, [], inst)
-  | Sil.Tvar _ ->
+  | Sil.Tarray _, Some len ->
+      Sil.Earray (len, [], inst)
+  | Sil.Tvar _, _
+  | (Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _), Some _ ->
       assert false
 
 (** Sil.Construct a pointsto. *)
@@ -1185,8 +1203,8 @@ let mk_ptsto lexp sexp te =
     initialize the fields of structs with fresh variables. *)
 let mk_ptsto_exp tenvo struct_init_mode (exp, te, expo) inst : Sil.hpred =
   let default_strexp () = match te with
-    | Sil.Sizeof (typ, _) ->
-        create_strexp_of_type tenvo struct_init_mode typ inst
+    | Sil.Sizeof (typ, len, _) ->
+        create_strexp_of_type tenvo struct_init_mode typ len inst
     | Sil.Var _ ->
         Sil.Estruct ([], inst)
     | te ->
@@ -1214,19 +1232,24 @@ let rec hpred_normalize sub hpred =
       let normalized_cnt = strexp_normalize sub cnt in
       let normalized_te = texp_normalize sub te in
       begin match normalized_cnt, normalized_te with
-        | Sil.Earray (Sil.Sizeof (t, st1), [], inst), Sil.Sizeof (Sil.Tarray _, _) ->
+        | Sil.Earray (Sil.Sizeof _ as size, [], inst), Sil.Sizeof (Sil.Tarray _, _, _) ->
             (* check for an empty array whose size expression is (Sizeof type), and turn the array
                into a strexp of the given type *)
-            let hpred' = mk_ptsto_exp None Fld_init (root, Sil.Sizeof (t, st1), None) inst in
+            let hpred' = mk_ptsto_exp None Fld_init (root, size, None) inst in
             replace_hpred hpred'
-        | Sil.Earray (Sil.BinOp(Sil.Mult, Sil.Sizeof (t, st1), x), esel, inst),
-          Sil.Sizeof (Sil.Tarray _, _)
-        | Sil.Earray (Sil.BinOp(Sil.Mult, x, Sil.Sizeof (t, st1)), esel, inst),
-          Sil.Sizeof (Sil.Tarray _, _) ->
-            (* check for an array whose size expression is n * (Sizeof type), and turn the array
-               into a strexp of the given type *)
-            let hpred' =
-              mk_ptsto_exp None Fld_init (root, Sil.Sizeof (Sil.Tarray(t, x), st1), None) inst in
+        | ( Sil.Earray (Sil.BinOp (Sil.Mult, Sil.Sizeof (t, None, st1), x), esel, inst)
+          | Sil.Earray (Sil.BinOp (Sil.Mult, x, Sil.Sizeof (t, None, st1)), esel, inst)),
+          Sil.Sizeof (Sil.Tarray (elt, _) as arr, _, _)
+          when Sil.typ_equal t elt ->
+            let len = Some x in
+            let hpred' = mk_ptsto_exp None Fld_init (root, Sil.Sizeof (arr, len, st1), None) inst in
+            replace_hpred (replace_array_contents hpred' esel)
+        | ( Sil.Earray (Sil.BinOp (Sil.Mult, Sil.Sizeof (t, Some len, st1), x), esel, inst)
+          | Sil.Earray (Sil.BinOp (Sil.Mult, x, Sil.Sizeof (t, Some len, st1)), esel, inst)),
+          Sil.Sizeof (Sil.Tarray (elt, _) as arr, _, _)
+          when Sil.typ_equal t elt ->
+            let len = Some (Sil.BinOp(Sil.Mult, x, len)) in
+            let hpred' = mk_ptsto_exp None Fld_init (root, Sil.Sizeof (arr, len, st1), None) inst in
             replace_hpred (replace_array_contents hpred' esel)
         | _ -> Sil.Hpointsto (normalized_root, normalized_cnt, normalized_te)
       end
@@ -1337,7 +1360,8 @@ let rec pi_sorted_remove_redundant = function
 let sigma_get_unsigned_exps sigma =
   let uexps = ref [] in
   let do_hpred = function
-    | Sil.Hpointsto(_, Sil.Eexp(e, _), Sil.Sizeof (Sil.Tint ik, _)) when Sil.ikind_is_unsigned ik ->
+    | Sil.Hpointsto (_, Sil.Eexp (e, _), Sil.Sizeof (Sil.Tint ik, _, _))
+      when Sil.ikind_is_unsigned ik ->
         uexps := e :: !uexps
     | _ -> () in
   IList.iter do_hpred sigma;
@@ -1622,13 +1646,13 @@ let get_fld_typ_path_opt src_exps snk_exp_ reachable_hpreds_ =
     | (_, Sil.Eexp (e, _)) -> Sil.exp_equal target_exp e
     | _ -> false in
   let extend_path hpred (snk_exp, path, reachable_hpreds) = match hpred with
-    | Sil.Hpointsto (lhs, Sil.Estruct (flds, _), Sil.Sizeof (typ, _)) ->
+    | Sil.Hpointsto (lhs, Sil.Estruct (flds, _), Sil.Sizeof (typ, _, _)) ->
         (try
            let fld, _ = IList.find (fun fld -> strexp_matches snk_exp fld) flds in
            let reachable_hpreds' = Sil.HpredSet.remove hpred reachable_hpreds in
            (lhs, (Some fld, typ) :: path, reachable_hpreds')
          with Not_found -> (snk_exp, path, reachable_hpreds))
-    | Sil.Hpointsto (lhs, Sil.Earray (_, elems, _), Sil.Sizeof (typ, _)) ->
+    | Sil.Hpointsto (lhs, Sil.Earray (_, elems, _), Sil.Sizeof (typ, _, _)) ->
         if IList.exists (fun pair -> strexp_matches snk_exp pair) elems
         then
           let reachable_hpreds' = Sil.HpredSet.remove hpred reachable_hpreds in
@@ -2039,7 +2063,8 @@ let find_arithmetic_problem proc_node_session prop exp =
     | Sil.Lvar _ -> ()
     | Sil.Lfield (e, _, _) -> walk e
     | Sil.Lindex (e1, e2) -> walk e1; walk e2
-    | Sil.Sizeof _ -> () in
+    | Sil.Sizeof (_, None, _) -> ()
+    | Sil.Sizeof (_, Some len, _) -> walk len in
   walk exp;
   try Some (Div0 (IList.find check_zero !exps_divided)), !res
   with Not_found ->
@@ -2320,7 +2345,8 @@ let rec exp_captured_ren ren = function
   | Sil.Var id -> Sil.Var (ident_captured_ren ren id)
   | Sil.Const (Sil.Cexn e) -> Sil.Const (Sil.Cexn (exp_captured_ren ren e))
   | Sil.Const _ as e -> e
-  | Sil.Sizeof (t, st) -> Sil.Sizeof (typ_captured_ren ren t, st)
+  | Sil.Sizeof (t, len, st) ->
+      Sil.Sizeof (typ_captured_ren ren t, Option.map (exp_captured_ren ren) len, st)
   | Sil.Cast (t, e) -> Sil.Cast (t, exp_captured_ren ren e)
   | Sil.UnOp (op, e, topt) ->
       let topt' = match topt with
diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli
index 575deb2fb..7cf63b087 100644
--- a/infer/src/backend/prop.mli
+++ b/infer/src/backend/prop.mli
@@ -221,7 +221,8 @@ val mk_neq : exp -> exp -> atom
 val mk_eq : exp -> exp -> atom
 
 (** create a strexp of the given type, populating the structures if [expand_structs] is true *)
-val create_strexp_of_type: Tenv.t option -> struct_init_mode -> Sil.typ -> Sil.inst -> Sil.strexp
+val create_strexp_of_type :
+  Tenv.t option -> struct_init_mode -> Sil.typ -> Sil.exp option -> Sil.inst -> Sil.strexp
 
 (** Construct a pointsto. *)
 val mk_ptsto : exp -> strexp -> exp -> hpred
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index ea0f665e2..50477a07d 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -371,7 +371,7 @@ end = struct
     let add_lt_minus1_e e =
       lts := (Sil.exp_minus_one, e)::!lts in
     let texp_is_unsigned = function
-      | Sil.Sizeof (Sil.Tint ik, _) -> Sil.ikind_is_unsigned ik
+      | Sil.Sizeof (Sil.Tint ik, _, _) -> Sil.ikind_is_unsigned ik
       | _ -> false in
     let strexp_lt_minus1 = function
       | Sil.Eexp (e, _) -> add_lt_minus1_e e
@@ -415,7 +415,8 @@ end = struct
     (* 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) -> Sil.Int.leq n1 n2
-    | Sil.BinOp (Sil.MinusA, Sil.Sizeof (t1, _), Sil.Sizeof (t2, _)), Sil.Const(Sil.Cint n2)
+    | Sil.BinOp (Sil.MinusA, Sil.Sizeof (t1, None, _), Sil.Sizeof (t2, None, _)),
+      Sil.Const(Sil.Cint n2)
       when Sil.Int.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] *)
@@ -1423,8 +1424,9 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred =
     | Sil.Hpointsto (Sil.Lfield (e, fld, typ_fld), se, t) ->
         let t' = match t, typ_fld with
           | _, Sil.Tstruct _ -> (* the struct type of fld is known *)
-              Sil.Sizeof (typ_fld, Sil.Subtype.exact)
-          | Sil.Sizeof (t1, st), _ -> (* the struct type of fld is not known -- typically Tvoid *)
+              Sil.Sizeof (typ_fld, None, Sil.Subtype.exact)
+          | Sil.Sizeof (t1, len, st), _ ->
+              (* the struct type of fld is not known -- typically Tvoid *)
               Sil.Sizeof
                 (Sil.Tstruct
                    { Sil.instance_fields = [(fld, t1, Sil.item_annotation_empty)];
@@ -1434,18 +1436,18 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred =
                      Sil.superclasses = [];
                      Sil.def_methods = [];
                      Sil.struct_annotations = Sil.item_annotation_empty;
-                   }, st)
+                   }, len, st)
           (* None as we don't know the stuct name *)
           | _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lfield") in
         let hpred' = Sil.Hpointsto (e, Sil.Estruct ([(fld, se)], Sil.inst_none), t') in
         expand true true hpred'
     | Sil.Hpointsto (Sil.Lindex (e, ind), se, t) ->
-        let size = Sil.exp_get_undefined false in
+        let clen = Sil.exp_get_undefined false in
         let t' = match t with
-          | Sil.Sizeof (_t, st) ->
-              Sil.Sizeof (Sil.Tarray (_t, size), st)
+          | Sil.Sizeof (t_, vlen, st) ->
+              Sil.Sizeof (Sil.Tarray (t_, clen), vlen, st)
           | _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in
-        let hpred' = Sil.Hpointsto (e, Sil.Earray (size, [(ind, se)], Sil.inst_none), t') in
+        let hpred' = Sil.Hpointsto (e, Sil.Earray (clen, [(ind, se)], Sil.inst_none), t') in
         expand true true hpred'
     | Sil.Hpointsto (Sil.BinOp (Sil.PlusPI, e1, e2), Sil.Earray (size, esel, inst), t) ->
         let shift_exp e = Sil.BinOp (Sil.PlusA, e, e2) in
@@ -1587,17 +1589,17 @@ struct
       case, if they are possible *)
   let subtype_case_analysis tenv texp1 texp2 =
     match texp1, texp2 with
-    | Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) ->
+    | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, len2, st2) ->
         begin
           let pos_opt, neg_opt = case_analysis_type tenv (t1, st1) (t2, st2) in
           let pos_type_opt = match pos_opt with
             | None -> None
             | Some st1' ->
-                let t1' = if check_subtype tenv t1 t2 then t1 else t2 in
-                Some (Sil.Sizeof (t1', st1')) in
+                let t1', len1' = if check_subtype tenv t1 t2 then t1, len1 else t2, len2 in
+                Some (Sil.Sizeof (t1', len1', st1')) in
           let neg_type_opt = match neg_opt with
             | None -> None
-            | Some st1' -> Some (Sil.Sizeof (t1, st1')) in
+            | Some st1' -> Some (Sil.Sizeof (t1, len1, st1')) in
           pos_type_opt, neg_type_opt
         end
     | _ -> (* don't know, consider both possibilities *)
@@ -1606,7 +1608,7 @@ end
 
 let cast_exception tenv texp1 texp2 e1 subs =
   let _ = match texp1, texp2 with
-    | Sil.Sizeof (t1, _), Sil.Sizeof (t2, st2) ->
+    | Sil.Sizeof (t1, _, _), Sil.Sizeof (t2, _, st2) ->
         if Config.developer_mode ||
            (Sil.Subtype.is_cast st2 &&
             not (Subtyping_check.check_subtype tenv t1 t2)) then
@@ -1636,8 +1638,10 @@ let get_overrides_of tenv supertype pname =
 
 (** Check the equality of two types ignoring flags in the subtyping components *)
 let texp_equal_modulo_subtype_flag texp1 texp2 = match texp1, texp2 with
-  | Sil.Sizeof(t1, st1), Sil.Sizeof (t2, st2) ->
-      Sil.typ_equal t1 t2 && Sil.Subtype.equal_modulo_flag st1 st2
+  | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, len2, st2) ->
+      Sil.typ_equal t1 t2
+      && (opt_equal Sil.exp_equal len1 len2)
+      && Sil.Subtype.equal_modulo_flag st1 st2
   | _ -> Sil.exp_equal texp1 texp2
 
 (** check implication between type expressions *)
@@ -1646,13 +1650,13 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
   (* classes and arrays in Java, and just classes in C++ and ObjC *)
   let types_subject_to_dynamic_cast =
     match texp1, texp2 with
-    | Sil.Sizeof ((Sil.Tstruct _) as typ1, _), Sil.Sizeof (Sil.Tstruct _, _)
-    | Sil.Sizeof ((Sil.Tarray _) as typ1, _), Sil.Sizeof (Sil.Tarray _, _)
-    | Sil.Sizeof ((Sil.Tarray _) as typ1, _), Sil.Sizeof (Sil.Tstruct _, _)
-    | Sil.Sizeof ((Sil.Tstruct _) as typ1, _), Sil.Sizeof (Sil.Tarray _, _)
+    | Sil.Sizeof ((Sil.Tstruct _) as typ1, _, _), Sil.Sizeof (Sil.Tstruct _, _, _)
+    | Sil.Sizeof ((Sil.Tarray _) as typ1, _, _), Sil.Sizeof (Sil.Tarray _, _, _)
+    | Sil.Sizeof ((Sil.Tarray _) as typ1, _, _), Sil.Sizeof (Sil.Tstruct _, _, _)
+    | Sil.Sizeof ((Sil.Tstruct _) as typ1, _, _), Sil.Sizeof (Sil.Tarray _, _, _)
       when is_java_class typ1 -> true
 
-    | Sil.Sizeof (typ1, _), Sil.Sizeof (typ2, _) ->
+    | Sil.Sizeof (typ1, _, _), Sil.Sizeof (typ2, _, _) ->
         (Sil.is_cpp_class typ1 && Sil.is_cpp_class typ2) ||
         (Sil.is_objc_class typ1 && Sil.is_objc_class typ2)
     | _ -> false in
@@ -1706,24 +1710,25 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2
   let type_rhs e =
     let sub_opt = ref None in
     let filter = function
-      | Sil.Hpointsto(e', _, Sil.Sizeof(t, sub)) when Sil.exp_equal e' e ->
-          sub_opt := Some (t, sub);
+      | Sil.Hpointsto(e', _, Sil.Sizeof(t, len, sub)) when Sil.exp_equal e' e ->
+          sub_opt := Some (t, len, sub);
           true
       | _ -> false in
     if IList.exists filter sigma2 then !sub_opt else None in
   let add_subtype () = match texp1, texp2, se1, se2 with
-    | Sil.Sizeof(Sil.Tptr (_t1, _), _), Sil.Sizeof(Sil.Tptr (_t2, _), _),
-      Sil.Eexp(e1', _), Sil.Eexp(e2', _)
+    | Sil.Sizeof (Sil.Tptr (t1_, _), None, _), Sil.Sizeof (Sil.Tptr (t2_, _), None, _),
+      Sil.Eexp (e1', _), Sil.Eexp (e2', _)
       when not (is_allocated_lhs e1') ->
         begin
-          let t1, t2 = Tenv.expand_type tenv _t1, Tenv.expand_type tenv _t2 in
+          let t1, t2 = Tenv.expand_type tenv t1_, Tenv.expand_type tenv t2_ in
           match type_rhs e2' with
-          | Some (t2_ptsto , sub2) ->
+          | Some (t2_ptsto, len2, sub2) ->
               if not (Sil.typ_equal t1 t2) && Subtyping_check.check_subtype tenv t1 t2
               then begin
                 let pos_type_opt, _ =
                   Subtyping_check.subtype_case_analysis tenv
-                    (Sil.Sizeof (t1, Sil.Subtype.subtypes)) (Sil.Sizeof (t2_ptsto, sub2)) in
+                    (Sil.Sizeof (t1, None, Sil.Subtype.subtypes))
+                    (Sil.Sizeof (t2_ptsto, len2, sub2)) in
                 match pos_type_opt with
                 | Some t1_noptr ->
                     ProverState.add_frame_typ (e1', t1_noptr);
@@ -1936,13 +1941,13 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
          | _ -> None)
     | _ -> None in
   let mk_constant_string_hpred s = (* create an hpred from a constant string *)
-    let size = Sil.exp_int (Sil.Int.of_int (1 + String.length s)) in
+    let len = Sil.exp_int (Sil.Int.of_int (1 + String.length s)) in
     let root = Sil.Const (Sil.Cstr s) in
     let sexp =
       let index = Sil.exp_int (Sil.Int.of_int (String.length s)) in
       match !Config.curr_language with
       | Config.Clang ->
-          Sil.Earray (size, [(index, Sil.Eexp (Sil.exp_zero, Sil.inst_none))], Sil.inst_none)
+          Sil.Earray (len, [(index, Sil.Eexp (Sil.exp_zero, Sil.inst_none))], Sil.inst_none)
       | Config.Java ->
           let mk_fld_sexp s =
             let fld = Ident.create_fieldname (Mangled.from_string s) 0 in
@@ -1952,14 +1957,15 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
           Sil.Estruct (IList.map mk_fld_sexp fields, Sil.inst_none) in
     let const_string_texp =
       match !Config.curr_language with
-      | Config.Clang -> Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, size), Sil.Subtype.exact)
+      | Config.Clang ->
+          Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, len), Some len, Sil.Subtype.exact)
       | Config.Java ->
           let object_type =
             Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.String") in
           let typ = match Tenv.lookup tenv object_type with
             | Some typ -> typ
             | None -> assert false in
-          Sil.Sizeof (Sil.Tstruct typ, Sil.Subtype.exact) in
+          Sil.Sizeof (Sil.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
@@ -1971,7 +1977,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
       let typ = match Tenv.lookup tenv class_type with
         | Some typ -> typ
         | None -> assert false in
-      Sil.Sizeof (Sil.Tstruct typ, Sil.Subtype.exact) in
+      Sil.Sizeof (Sil.Tstruct typ, None, Sil.Subtype.exact) in
     Sil.Hpointsto (root, sexp, class_texp) in
   try
     (match move_primed_lhs_from_front subs sigma2 with
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index 52e2431a8..f9aef8ead 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -392,10 +392,11 @@ let strexp_extend_values
     let check_not_inconsistent (atoms, _, _) = not (IList.exists check_neg_atom atoms) in
     IList.filter check_not_inconsistent atoms_se_typ_list in
   if Config.trace_rearrange then L.d_strln "exiting strexp_extend_values";
-  let st = match te with
-    | Sil.Sizeof(_, st) -> st
-    | _ -> Sil.Subtype.exact in
-  IList.map (fun (atoms', se', typ') -> (laundry_atoms @ atoms', se', Sil.Sizeof (typ', st))) atoms_se_typ_list_filtered
+  let len, st = match te with
+    | Sil.Sizeof(_, len, st) -> (len, st)
+    | _ -> None, Sil.Subtype.exact in
+  IList.map (fun (atoms', se', typ') -> (laundry_atoms @ atoms', se', Sil.Sizeof (typ', len, st)))
+    atoms_se_typ_list_filtered
 
 let collect_root_offset exp =
   let root = Sil.root_of_lexp exp in
@@ -430,17 +431,17 @@ let mk_ptsto_exp_footprint
     | Sil.Lvar pvar, [], Sil.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
-        ([], Prop.mk_ptsto root (Sil.Eexp (fun_exp, inst)) (Sil.Sizeof (typ, st)))
+        ([], Prop.mk_ptsto root (Sil.Eexp (fun_exp, inst)) (Sil.Sizeof (typ, None, st)))
     | _, [], Sil.Tfun _ ->
         let atoms, se, t =
           create_struct_values
             pname tenv orig_prop footprint_part Ident.kfootprint max_stamp typ off0 inst in
-        (atoms, Prop.mk_ptsto root se (Sil.Sizeof (t, st)))
+        (atoms, Prop.mk_ptsto root se (Sil.Sizeof (t, None, st)))
     | _ ->
         let atoms, se, t =
           create_struct_values
             pname tenv orig_prop footprint_part Ident.kfootprint max_stamp typ off0 inst in
-        (atoms, Prop.mk_ptsto root se (Sil.Sizeof (t, st))) in
+        (atoms, Prop.mk_ptsto root se (Sil.Sizeof (t, None, st))) in
   let atoms, ptsto_foot = create_ptsto true off_foot in
   let sub = Sil.sub_of_list eqs in
   let ptsto = Sil.hpred_sub sub ptsto_foot in
@@ -709,7 +710,7 @@ let add_guarded_by_constraints prop lexp pdesc =
     | _ ->
         prop_acc in
   let hpred_check_flds prop_acc = function
-    | Sil.Hpointsto (_, Estruct (flds, _), Sizeof (typ, _)) ->
+    | Sil.Hpointsto (_, Estruct (flds, _), Sizeof (typ, _, _)) ->
         IList.fold_left (check_fld_locks typ) prop_acc flds
     | _ ->
         prop_acc in
@@ -926,7 +927,7 @@ let type_at_offset texp off =
         strip_offset off' typ'
     | _ -> None in
   match texp with
-  | Sil.Sizeof(typ, _) ->
+  | Sil.Sizeof(typ, _, _) ->
       strip_offset off typ
   | _ -> None
 
@@ -1080,7 +1081,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
                  IList.exists is_nullable_attr (Prop.get_exp_attributes prop exp) in
              (* it's ok for a non-nullable local to point to deref_exp *)
              is_nullable || Pvar.is_local pvar
-         | Sil.Hpointsto (_, Sil.Estruct (flds, _), Sil.Sizeof (typ, _)) ->
+         | Sil.Hpointsto (_, Sil.Estruct (flds, _), Sil.Sizeof (typ, _, _)) ->
              let fld_is_nullable fld =
                match Annotations.get_field_type_and_annotation fld typ with
                | Some (_, annot) -> Annotations.ia_is_nullable annot
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 253df711c..526dfcd3d 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -128,7 +128,7 @@ let rec apply_offlist
       else
         begin
           L.d_strln "WARNING: struct assignment treated as nondeterministic assignment";
-          (f None, Prop.create_strexp_of_type (Some tenv) Prop.Fld_init typ inst, typ, None)
+          (f None, Prop.create_strexp_of_type (Some tenv) Prop.Fld_init typ None inst, typ, None)
         end
   | [], Sil.Earray _ ->
       let offlist' = (Sil.Off_index Sil.exp_zero):: offlist in
@@ -213,7 +213,7 @@ let rec apply_offlist
     Finally, before running this function, the tool should run strexp_extend_value
     in rearrange.ml for the same se and offlist, so that all the necessary
     extensions of se are done before this function. *)
-let ptsto_lookup pdesc tenv p (lexp, se, typ, st) offlist id =
+let ptsto_lookup pdesc tenv p (lexp, se, typ, len, st) offlist id =
   let f =
     function Some exp -> exp | None -> Sil.Var id in
   let fp_root =
@@ -226,7 +226,7 @@ let ptsto_lookup pdesc tenv p (lexp, se, typ, st) offlist id =
     match !lookup_inst with
     | Some (Sil.Iinitial | Sil.Ialloc | Sil.Ilookup) -> true
     | _ -> false in
-  let ptsto' = Prop.mk_ptsto lexp se' (Sil.Sizeof (typ', st)) in
+  let ptsto' = Prop.mk_ptsto lexp se' (Sil.Sizeof (typ', len, st)) in
   (e', ptsto', pred_insts_op', lookup_uninitialized)
 
 (** [ptsto_update p (lexp,se,typ) offlist exp] takes
@@ -240,7 +240,7 @@ let ptsto_lookup pdesc tenv p (lexp, se, typ, st) offlist id =
     the tool should run strexp_extend_value in rearrange.ml for the same
     se and offlist, so that all the necessary extensions of se are done
     before this function. *)
-let ptsto_update pdesc tenv p (lexp, se, typ, st) offlist exp =
+let ptsto_update pdesc tenv p (lexp, se, typ, len, st) offlist exp =
   let f _ = exp in
   let fp_root =
     match lexp with Sil.Var id -> Ident.is_footprint id | _ -> false in
@@ -249,7 +249,7 @@ let ptsto_update pdesc tenv p (lexp, se, typ, st) offlist exp =
     let pos = State.get_path_pos () in
     apply_offlist
       pdesc tenv p fp_root true (lexp, se, typ) offlist f (State.get_inst_update pos) lookup_inst in
-  let ptsto' = Prop.mk_ptsto lexp se' (Sil.Sizeof (typ', st)) in
+  let ptsto' = Prop.mk_ptsto lexp se' (Sil.Sizeof (typ', len, st)) in
   (ptsto', pred_insts_op')
 
 let update_iter iter pi sigma =
@@ -526,8 +526,8 @@ let resolve_typename prop receiver_exp =
       | _ :: hpreds -> loop hpreds in
     loop (Prop.get_sigma prop) in
   match typexp_opt with
-  | Some (Sil.Sizeof (Sil.Tstruct { Sil.struct_name = None }, _)) -> None
-  | Some (Sil.Sizeof (Sil.Tstruct { Sil.csu = Csu.Class ck; struct_name = Some name }, _)) ->
+  | Some (Sil.Sizeof (Sil.Tstruct { Sil.struct_name = None }, _, _)) -> None
+  | Some (Sil.Sizeof (Sil.Tstruct { Sil.csu = Csu.Class ck; struct_name = Some name }, _, _)) ->
       Some (Typename.TN_csu (Csu.Class ck, name))
   | _ -> None
 
@@ -777,7 +777,7 @@ let do_error_checks node_opt instr pname pdesc = match node_opt with
 let add_strexp_to_footprint strexp abducted_pv typ prop =
   let abducted_lvar = Sil.Lvar abducted_pv in
   let lvar_pt_fpvar =
-    let sizeof_exp = Sil.Sizeof (typ, Sil.Subtype.subtypes) in
+    let sizeof_exp = Sil.Sizeof (typ, None, Sil.Subtype.subtypes) in
     Prop.mk_ptsto abducted_lvar strexp sizeof_exp in
   let sigma_fp = Prop.get_sigma_footprint prop in
   Prop.normalize (Prop.replace_sigma_footprint (lvar_pt_fpvar :: sigma_fp) prop)
@@ -793,7 +793,7 @@ let add_to_footprint abducted_pv typ prop =
    footprint. we can get rid of this special case if we fix the abduction on struct values *)
 let add_struct_value_to_footprint tenv abducted_pv typ prop =
   let struct_strexp =
-    Prop.create_strexp_of_type (Some tenv) Prop.Fld_init typ Sil.inst_none in
+    Prop.create_strexp_of_type (Some tenv) Prop.Fld_init typ None Sil.inst_none in
   let prop' = add_strexp_to_footprint struct_strexp abducted_pv typ prop in
   prop', struct_strexp
 
@@ -876,9 +876,9 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
     let iter_ren = Prop.prop_iter_make_id_primed id iter in
     let prop_ren = Prop.prop_iter_to_prop iter_ren in
     match Prop.prop_iter_current iter_ren with
-    | (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, st)), offlist) ->
+    | (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, len, st)), offlist) ->
         let contents, new_ptsto, pred_insts_op, lookup_uninitialized =
-          ptsto_lookup pdesc tenv prop_ren (lexp, strexp, typ, st) offlist id in
+          ptsto_lookup pdesc tenv prop_ren (lexp, strexp, typ, len, st) offlist id in
         let update acc (pi, sigma) =
           let pi' = Sil.Aeq (Sil.Var(id), contents):: pi in
           let sigma' = new_ptsto:: sigma in
@@ -948,14 +948,14 @@ let load_ret_annots pname =
 
 let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp loc prop_ =
   let execute_set_ pdesc tenv rhs_exp acc_in iter =
-    let (lexp, strexp, typ, st, offlist) =
+    let (lexp, strexp, typ, len, st, offlist) =
       match Prop.prop_iter_current iter with
-      | (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, st)), offlist) ->
-          (lexp, strexp, typ, st, offlist)
+      | (Sil.Hpointsto(lexp, strexp, Sil.Sizeof (typ, len, st)), offlist) ->
+          (lexp, strexp, typ, len, st, offlist)
       | _ -> assert false in
     let p = Prop.prop_iter_to_prop iter in
     let new_ptsto, pred_insts_op =
-      ptsto_update pdesc tenv p (lexp, strexp, typ, st) offlist rhs_exp in
+      ptsto_update pdesc tenv p (lexp, strexp, typ, len, st) offlist rhs_exp in
     let update acc (pi, sigma) =
       let sigma' = new_ptsto:: sigma in
       let iter' = update_iter iter pi sigma' in
@@ -1058,7 +1058,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
             let lhs_is_ns_ptr () =
               IList.exists
                 (function
-                  | Sil.Hpointsto (_, Sil.Eexp (exp, _), Sil.Sizeof (Sil.Tptr (typ, _), _)) ->
+                  | Sil.Hpointsto (_, Sil.Eexp (exp, _), Sil.Sizeof (Sil.Tptr (typ, _), _, _)) ->
                       Sil.exp_equal exp lhs_normal && is_nsnumber typ
                   | _ -> false)
                 (Prop.get_sigma prop__) in
@@ -1242,7 +1242,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       ret_old_path [Prop.exist_quantify (Sil.fav_from_list temps) prop_]
   | Sil.Declare_locals (ptl, _) ->
       let sigma_locals =
-        let add_None (x, y) = (x, Sil.Sizeof (y, Sil.Subtype.exact), None) in
+        let add_None (x, y) = (x, Sil.Sizeof (y, None, Sil.Subtype.exact), None) in
         let sigma_locals () =
           IList.map
             (Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_initial)
@@ -1353,7 +1353,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
     let havoc_actual_by_ref (actual, actual_typ) prop =
       let actual_pt_havocd_var =
         let havocd_var = Sil.Var (Ident.create_fresh Ident.kprimed) in
-        let sizeof_exp = Sil.Sizeof (Sil.typ_strip_ptr actual_typ, Sil.Subtype.subtypes) in
+        let sizeof_exp = Sil.Sizeof (Sil.typ_strip_ptr actual_typ, None, Sil.Subtype.subtypes) in
         Prop.mk_ptsto actual (Sil.Eexp (havocd_var, Sil.Inone)) sizeof_exp in
       replace_actual_hpred actual actual_pt_havocd_var prop in
     IList.fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index aa44ecc49..52daf6af2 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -473,8 +473,8 @@ let texp_star texp1 texp2 =
         if ftal_sub instance_fields1 instance_fields2 then t2 else t1
     | _ -> t1 in
   match texp1, texp2 with
-  | Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) ->
-      Sil.Sizeof (typ_star t1 t2, Sil.Subtype.join st1 st2)
+  | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, _, st2) ->
+      Sil.Sizeof (typ_star t1 t2, len1, Sil.Subtype.join st1 st2)
   | _ ->
       texp1
 
@@ -629,7 +629,7 @@ let prop_get_exn_name pname prop =
   let ret_pvar = Sil.Lvar (Pvar.get_ret_pvar pname) in
   let rec search_exn e = function
     | [] -> None
-    | Sil.Hpointsto (e1, _, Sil.Sizeof (Sil.Tstruct  { Sil.struct_name = Some name }, _)) :: _
+    | Sil.Hpointsto (e1, _, Sil.Sizeof (Sil.Tstruct  { Sil.struct_name = Some name }, _, _)) :: _
       when Sil.exp_equal e1 e ->
         Some (Typename.TN_csu (Csu.Class Csu.Java, name))
     | _ :: tl -> search_exn e tl in
@@ -868,7 +868,7 @@ let mk_actual_precondition prop actual_params formal_params =
     Prop.mk_ptsto
       (Sil.Lvar formal_var)
       (Sil.Eexp (actual_e, Sil.inst_actual_precondition))
-      (Sil.Sizeof (actual_t, Sil.Subtype.exact)) in
+      (Sil.Sizeof (actual_t, None, Sil.Subtype.exact)) in
   let instantiated_formals = IList.map mk_instantiation formals_actuals in
   let actual_pre = Prop.prop_sigma_star prop instantiated_formals in
   Prop.normalize actual_pre
diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml
index 3f9154e92..f68f40eaf 100644
--- a/infer/src/backend/utils.ml
+++ b/infer/src/backend/utils.ml
@@ -48,6 +48,13 @@ let opt_equal cmp x1 x2 = match x1, x2 with
   | None, Some _ -> false
   | Some y1, Some y2 -> cmp y1 y2
 
+let opt_compare cmp x1 x2 =
+  match x1, x2 with
+  | Some y1, Some y2 -> cmp y1 y2
+  | None, None -> 0
+  | None, _ -> -1
+  | _, None -> 1
+
 (** Efficient comparison for integers *)
 let int_compare (i: int) (j: int) = i - j
 
@@ -64,6 +71,10 @@ let triple_compare compare compare' compare'' (x1, y1, z1) (x2, y2, z2) =
   if n <> 0 then n else let n = compare' y1 y2 in
     if n <> 0 then n else compare'' z1 z2
 
+let fst3 (x,_,_) = x
+let snd3 (_,x,_) = x
+let trd3 (_,_,x) = x
+
 (** {2 Useful Modules} *)
 
 (** Set of integers *)
diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli
index 31098c46e..995dd8ee6 100644
--- a/infer/src/backend/utils.mli
+++ b/infer/src/backend/utils.mli
@@ -44,6 +44,9 @@ val int_equal : int -> int -> bool
 (** Extend and equality function to an option type. *)
 val opt_equal : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
 
+(** Comparison of option type. *)
+val opt_compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int
+
 (** Generic comparison of pairs given a compare function for each element of the pair. *)
 val pair_compare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('a * 'c) -> ('b * 'd) -> int
 
@@ -59,6 +62,15 @@ val string_equal : string -> string -> bool
 (** Comparison for floats *)
 val float_compare : float -> float -> int
 
+(** Return the first component of a triple. *)
+val fst3 : 'a * 'b * 'c -> 'a
+
+(** Return the second component of a triple. *)
+val snd3 : 'a * 'b * 'c -> 'b
+
+(** Return the third component of a triple. *)
+val trd3 : 'a * 'b * 'c -> 'c
+
 (** {2 Useful Modules} *)
 
 (** Set of integers *)
diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml
index 964a8be2c..5b0e919c7 100644
--- a/infer/src/clang/cTrans.ml
+++ b/infer/src/clang/cTrans.ml
@@ -216,7 +216,7 @@ struct
         CTypes_decl.objc_class_name_to_sil_type trans_state.context.CContext.tenv class_name in
       let expanded_type = CTypes.expand_structured_type trans_state.context.CContext.tenv typ in
       { empty_res_trans with
-        exps = [(Sil.Sizeof(expanded_type, Sil.Subtype.exact), Sil.Tint Sil.IULong)] }
+        exps = [(Sil.Sizeof(expanded_type, None, Sil.Subtype.exact), Sil.Tint Sil.IULong)] }
 
   let add_reference_if_glvalue typ expr_info =
     (* glvalue definition per C++11:*)
@@ -426,7 +426,8 @@ struct
           match tp with
           | Some tp -> CTypes_decl.type_ptr_to_sil_type tenv tp
           | None -> typ in (* Some default type since the type is missing *)
-        { empty_res_trans with exps = [(Sil.Sizeof(sizeof_typ, Sil.Subtype.exact), sizeof_typ)]}
+        { empty_res_trans with
+          exps = [(Sil.Sizeof (sizeof_typ, None, Sil.Subtype.exact), sizeof_typ)] }
     | k -> Printing.log_stats
              "\nWARNING: Missing translation of Uniry_Expression_Or_Trait of kind: \
               %s . Expression ignored, returned -1... \n"
@@ -2189,7 +2190,7 @@ struct
     let sil_loc = CLocation.get_sil_location stmt_info context in
     let cast_type = CTypes_decl.type_ptr_to_sil_type tenv cast_type_ptr in
     let sizeof_expr = match cast_type with
-      | Sil.Tptr (typ, _) -> Sil.Sizeof (typ, subtypes)
+      | Sil.Tptr (typ, _) -> Sil.Sizeof (typ, None, subtypes)
       | _ -> assert false in
     let builtin = Sil.Const (Sil.Cfun ModelBuiltins.__cast) in
     let stmt = match stmts with [stmt] -> stmt | _ -> assert false in
@@ -2247,7 +2248,7 @@ struct
     let fun_name = ModelBuiltins.__cxx_typeid in
     let sil_fun = Sil.Const (Sil.Cfun fun_name) in
     let ret_id = Ident.create_fresh Ident.knormal in
-    let type_info_objc = (Sil.Sizeof (typ, Sil.Subtype.exact), Sil.Tvoid) in
+    let type_info_objc = (Sil.Sizeof (typ, None, Sil.Subtype.exact), Sil.Tvoid) in
     let field_name_decl = Ast_utils.make_qual_name_decl ["type_info"; "std"] "__type_name" in
     let field_name = General_utils.mk_class_field_name field_name_decl in
     let ret_exp = Sil.Var ret_id in
diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml
index 351a6d23f..9864ad56b 100644
--- a/infer/src/clang/cTrans_utils.ml
+++ b/infer/src/clang/cTrans_utils.ml
@@ -296,7 +296,7 @@ let create_alloc_instrs context sil_loc function_type fname size_exp_opt procnam
         function_type, styp
     | _ -> Sil.Tptr (function_type, Sil.Pk_pointer), function_type in
   let function_type_np = CTypes.expand_structured_type context.CContext.tenv function_type_np in
-  let sizeof_exp_ = Sil.Sizeof (function_type_np, Sil.Subtype.exact) in
+  let sizeof_exp_ = Sil.Sizeof (function_type_np, None, Sil.Subtype.exact) in
   let sizeof_exp = match size_exp_opt with
     | Some exp -> Sil.BinOp (Sil.Mult, sizeof_exp_, exp)
     | None -> sizeof_exp_ in
@@ -366,7 +366,7 @@ let create_cast_instrs context exp cast_from_typ cast_to_typ sil_loc =
   let ret_id = Ident.create_fresh Ident.knormal in
   let typ = CTypes.remove_pointer_to_typ cast_to_typ in
   let cast_typ_no_pointer = CTypes.expand_structured_type context.CContext.tenv typ in
-  let sizeof_exp = Sil.Sizeof (cast_typ_no_pointer, Sil.Subtype.exact) in
+  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, Sil.Tint Sil.IULong)] in
   let stmt_call = Sil.Call([ret_id], (Sil.Const (Sil.Cfun pname)), args, sil_loc, Sil.cf_default) in
diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml
index 749322a8e..bdc0d0c75 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 (Sil.Cfun pn), [_; (Sil.Sizeof(t, _, _), _)], _, _) when
           Procname.equal pn ModelBuiltins.__instanceof && typ_is_throwable t ->
           throwable_found := true
       | _ -> () in
diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml
index 3ebedfdb2..362711485 100644
--- a/infer/src/harness/inhabit.ml
+++ b/infer/src/harness/inhabit.ml
@@ -68,12 +68,12 @@ let get_non_receiver_formals formals = tl_or_empty formals
 (** create Sil corresponding to x = new typ() or x = new typ[]. For ordinary allocation, sizeof_typ
  * and ret_typ should be the same, but arrays are slightly odd in that sizeof_typ will have a size
  * component but the size component of ret_typ is always -1. *)
-let inhabit_alloc sizeof_typ ret_typ alloc_kind env =
+let inhabit_alloc sizeof_typ sizeof_len ret_typ alloc_kind env =
   let retval = Ident.create_fresh Ident.knormal in
   let inhabited_exp = Sil.Var retval in
   let call_instr =
     let fun_new = fun_exp_from_name alloc_kind in
-    let sizeof_exp = Sil.Sizeof (sizeof_typ, Sil.Subtype.exact) in
+    let sizeof_exp = Sil.Sizeof (sizeof_typ, sizeof_len, Sil.Subtype.exact) in
     let args = [(sizeof_exp, Sil.Tptr (ret_typ, Sil.Pk_pointer))] in
     Sil.Call ([retval], fun_new, args, env.pc, cf_alloc) in
   (inhabited_exp, env_add_instr call_instr env)
@@ -87,11 +87,11 @@ let rec inhabit_typ typ cfg env =
       | Sil.Tptr (Sil.Tarray (inner_typ, Sil.Const (Sil.Cint _)), Sil.Pk_pointer) ->
           let arr_size = Sil.Const (Sil.Cint (Sil.Int.one)) in
           let arr_typ = Sil.Tarray (inner_typ, arr_size) in
-          inhabit_alloc arr_typ typ ModelBuiltins.__new_array env
+          inhabit_alloc arr_typ (Some arr_size) typ ModelBuiltins.__new_array env
       | Sil.Tptr (typ, Sil.Pk_pointer) as ptr_to_typ ->
           (* TODO (t4575417): this case does not work correctly for enums, but they are currently
            * broken in Infer anyway (see t4592290) *)
-          let (allocated_obj_exp, env) = inhabit_alloc typ typ ModelBuiltins.__new env in
+          let (allocated_obj_exp, env) = inhabit_alloc typ None typ ModelBuiltins.__new env in
           (* select methods that are constructors and won't force us into infinite recursion because
            * we are already inhabiting one of their argument types *)
           let get_all_suitable_constructors typ = match typ with
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index e370eaf51..dd54191be 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -645,10 +645,11 @@ let get_array_size context pc expr_list content_type =
     | (other_instrs, other_exprs) ->
         (instrs@other_instrs, sil_size_expr:: other_exprs) in
   let (instrs, sil_size_exprs) = (IList.fold_right get_expr_instr expr_list ([],[])) in
-  let get_array_type sil_size_expr content_type =
-    Sil.Tarray (content_type, sil_size_expr) in
-  let array_type = (IList.fold_right get_array_type sil_size_exprs content_type) in
-  let array_size = Sil.Sizeof (array_type, Sil.Subtype.exact) in
+  let get_array_type_len sil_size_expr (content_type, _) =
+    (Sil.Tarray (content_type, sil_size_expr), Some sil_size_expr) in
+  let array_type, array_len =
+    IList.fold_right get_array_type_len sil_size_exprs (content_type, None) in
+  let array_size = Sil.Sizeof (array_type, array_len, Sil.Subtype.exact) in
   (instrs, array_size)
 
 module Int =
@@ -902,7 +903,7 @@ let rec instruction context pc instr : translation =
         let builtin_new = Sil.Const (Sil.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, Sil.Subtype.exact) in
+        let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in
         let args = [(sizeof_exp, class_type)] in
         let ret_id = Ident.create_fresh Ident.knormal in
         let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
@@ -1016,7 +1017,7 @@ let rec instruction context pc instr : translation =
           and npe_cn = JBasics.make_cn JConfig.npe_cl in
           let class_type = JTransType.get_class_type program tenv npe_cn
           and class_type_np = JTransType.get_class_type_no_pointer program tenv npe_cn in
-          let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in
+          let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in
           let args = [(sizeof_exp, class_type)] in
           let ret_id = Ident.create_fresh Ident.knormal in
           let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
@@ -1069,7 +1070,7 @@ let rec instruction context pc instr : translation =
           let out_of_bound_cn = JBasics.make_cn JConfig.out_of_bound_cl in
           let class_type = JTransType.get_class_type program tenv out_of_bound_cn
           and class_type_np = JTransType.get_class_type_no_pointer program tenv out_of_bound_cn in
-          let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in
+          let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in
           let args = [(sizeof_exp, class_type)] in
           let ret_id = Ident.create_fresh Ident.knormal in
           let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
@@ -1108,7 +1109,7 @@ let rec instruction context pc instr : translation =
           and cce_cn = JBasics.make_cn JConfig.cce_cl in
           let class_type = JTransType.get_class_type program tenv cce_cn
           and class_type_np = JTransType.get_class_type_no_pointer program tenv cce_cn in
-          let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in
+          let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in
           let args = [(sizeof_exp, class_type)] in
           let ret_id = Ident.create_fresh Ident.knormal in
           let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml
index 356535377..5dadc8ce1 100644
--- a/infer/src/java/jTransExn.ml
+++ b/infer/src/java/jTransExn.ml
@@ -67,7 +67,9 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table =
         let id_instanceof = Ident.create_fresh Ident.knormal in
         let instr_call_instanceof =
           let instanceof_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__instanceof) in
-          let args = [(Sil.Var id_exn_val, Sil.Tptr(exn_type, Sil.Pk_pointer)); (Sil.Sizeof (exn_type, Sil.Subtype.exact), Sil.Tvoid)] in
+          let args = [
+            (Sil.Var id_exn_val, Sil.Tptr(exn_type, Sil.Pk_pointer));
+            (Sil.Sizeof (exn_type, None, Sil.Subtype.exact), Sil.Tvoid)] in
           Sil.Call ([id_instanceof], instanceof_builtin, args, loc, Sil.cf_default) in
         let if_kind = Sil.Ik_switch in
         let instr_prune_true = Sil.Prune (Sil.Var id_instanceof, loc, true, if_kind) in
diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml
index cf6f2319a..ac206d62f 100644
--- a/infer/src/java/jTransType.ml
+++ b/infer/src/java/jTransType.ml
@@ -397,11 +397,11 @@ and value_type program tenv vt =
 (**  Translate object types into Sil.Sizeof expressions *)
 let sizeof_of_object_type program tenv ot subtypes =
   match object_type program tenv ot with
-  | Sil.Tptr (Sil.Tarray (vtyp, s), Sil.Pk_pointer) ->
-      let typ = (Sil.Tarray (vtyp, s)) in
-      Sil.Sizeof (typ, subtypes)
+  | Sil.Tptr (Sil.Tarray (vtyp, len), Sil.Pk_pointer) ->
+      let typ = (Sil.Tarray (vtyp, len)) in
+      Sil.Sizeof (typ, Some len, subtypes)
   | Sil.Tptr (typ, _) ->
-      Sil.Sizeof (typ, subtypes)
+      Sil.Sizeof (typ, None, subtypes)
   | _ ->
       raise (Type_tranlsation_error "Pointer or array type expected in tenv")