diff --git a/infer/models/c/src/glib.c b/infer/models/c/src/glib.c
index 078124bde..79c1beeb1 100644
--- a/infer/models/c/src/glib.c
+++ b/infer/models/c/src/glib.c
@@ -33,11 +33,11 @@ void* g_realloc(void* ptr, size_t size) {
     return NULL;
   }
   int old_size;
-  old_size = __get_array_size(ptr); // force ptr to be an array
+  old_size = __get_array_length(ptr); // force ptr to be an array
   int can_enlarge; // nondeterministically choose whether the current block can
   // be enlarged
   if (can_enlarge) {
-    __set_array_size(ptr, size); // enlarge the block
+    __set_array_length(ptr, size); // enlarge the block
     return ptr;
   }
   int* newblock = (int*)malloc(size);
diff --git a/infer/models/c/src/infer_builtins.h b/infer/models/c/src/infer_builtins.h
index 6cca798a7..ce0a1bcfe 100644
--- a/infer/models/c/src/infer_builtins.h
+++ b/infer/models/c/src/infer_builtins.h
@@ -61,13 +61,13 @@ clock_t __infer_nondet_clock_t();
 extern void __require_allocated_array(const void* arr);
 
 // builtin: return the size of arr
-extern size_t __get_array_size(const void* arr);
+extern size_t __get_array_length(const void* arr);
 
 // builtin: change the attribute of ret to a file attribute
 extern void __set_file_attribute(void* ret);
 
 // builtin: change the size of the array to size
-extern void __set_array_size(void* ptr, size_t size);
+extern void __set_array_length(void* ptr, size_t size);
 
 // builtin: set the flag to the given value for the procedure where this call
 // appears
diff --git a/infer/models/c/src/libc_basic.c b/infer/models/c/src/libc_basic.c
index e636e5df1..826ab7bfa 100644
--- a/infer/models/c/src/libc_basic.c
+++ b/infer/models/c/src/libc_basic.c
@@ -84,9 +84,9 @@ char* strcpy(char* s1, const char* s2) {
   __infer_set_flag("ignore_return",
                    ""); // no warnings if the return value is ignored
   __require_allocated_array(s1);
-  size1 = __get_array_size(s1);
+  size1 = __get_array_length(s1);
   __require_allocated_array(s2);
-  size2 = __get_array_size(s2);
+  size2 = __get_array_length(s2);
   INFER_EXCLUDE_CONDITION(size2 > size1);
   return s1;
 }
@@ -96,7 +96,7 @@ char* strcpy(char* s1, const char* s2) {
 char* strdup(const char* s) {
   int size;
   __require_allocated_array(s);
-  size = __get_array_size(s);
+  size = __get_array_length(s);
   return (char*)malloc(size);
 }
 
@@ -106,9 +106,9 @@ char* strcat(char* s1, const char* s2) {
   int size1;
   int size2;
   __require_allocated_array(s1);
-  size1 = __get_array_size(s1);
+  size1 = __get_array_length(s1);
   __require_allocated_array(s2);
-  size2 = __get_array_size(s2);
+  size2 = __get_array_length(s2);
   INFER_EXCLUDE_CONDITION(size2 > size1);
   return s1;
 }
@@ -133,7 +133,7 @@ char* strchr(char* s, int c) throw() {
   offset = __infer_nondet_int();
 
   __require_allocated_array(s);
-  size = __get_array_size(s);
+  size = __get_array_length(s);
   if (nondet)
     return 0;
   INFER_EXCLUDE_CONDITION(offset < 0 || offset >= size);
@@ -167,7 +167,7 @@ int strcmp(const char* s1, const char* s2) {
 size_t strlen(const char* s) {
   int size;
   __require_allocated_array(s);
-  size = __get_array_size(s);
+  size = __get_array_length(s);
   return size - 1;
 }
 
@@ -185,9 +185,9 @@ char* strncat(char* s1, const char* s2, size_t n) {
   int size_s1;
   int size_s2;
   __require_allocated_array(s1);
-  size_s1 = __get_array_size(s1);
+  size_s1 = __get_array_length(s1);
   __require_allocated_array(s2);
-  size_s2 = __get_array_size(s2);
+  size_s2 = __get_array_length(s2);
   INFER_EXCLUDE_CONDITION((n > size_s1) || (n > size_s2));
   return s1;
 }
@@ -201,9 +201,9 @@ int strncmp(const char* s1, const char* s2, size_t n) {
   int res;
   res = __infer_nondet_int();
   __require_allocated_array(s1);
-  size_s1 = __get_array_size(s1);
+  size_s1 = __get_array_length(s1);
   __require_allocated_array(s2);
-  size_s2 = __get_array_size(s2);
+  size_s2 = __get_array_length(s2);
   INFER_EXCLUDE_CONDITION((n > size_s1) || (n > size_s2));
   return res;
 }
@@ -216,7 +216,7 @@ char* strncpy(char* s1, const char* s2, size_t n) {
   __infer_set_flag("ignore_return",
                    ""); // no warnings if the return value is ignored
   __require_allocated_array(s1);
-  size1 = __get_array_size(s1);
+  size1 = __get_array_length(s1);
   __require_allocated_array(s2);
   INFER_EXCLUDE_CONDITION(n > size1);
   return s1;
@@ -237,7 +237,7 @@ char* strpbrk(char* s1, const char* s2) throw() {
   nondet = __infer_nondet_int();
   offset = __infer_nondet_int();
   __require_allocated_array(s1);
-  size1 = __get_array_size(s1);
+  size1 = __get_array_length(s1);
   __require_allocated_array(s2);
   if (nondet)
     return 0;
@@ -252,7 +252,7 @@ size_t strspn(const char* s1, const char* s2) {
   int res;
   res = __infer_nondet_int();
   __require_allocated_array(s1);
-  size_s1 = __get_array_size(s1);
+  size_s1 = __get_array_length(s1);
   __require_allocated_array(s2);
   INFER_EXCLUDE_CONDITION(res < 0 || res > size_s1);
   return res;
@@ -274,7 +274,7 @@ char* strstr(char* s1, const char* s2) throw() {
   nondet = __infer_nondet_int();
   offset = __infer_nondet_int();
   __require_allocated_array(s1);
-  size1 = __get_array_size(s1);
+  size1 = __get_array_length(s1);
   __require_allocated_array(s2);
   if (nondet)
     return 0;
@@ -300,7 +300,7 @@ unsigned long strtoul(const char* str, char** endptr, int base) {
   int offset;
   int res;
   __require_allocated_array(str);
-  size = __get_array_size(str);
+  size = __get_array_length(str);
   offset = __infer_nondet_int();
   INFER_EXCLUDE_CONDITION(offset < 0 || offset >= size);
   if (endptr)
@@ -338,7 +338,7 @@ void* memchr(void* s, int c, size_t n) throw() {
   nondet = __infer_nondet_int();
   offset = __infer_nondet_int();
   __require_allocated_array(s);
-  size = __get_array_size(s);
+  size = __get_array_length(s);
   INFER_EXCLUDE_CONDITION(n > size);
   if (nondet)
     return 0;
@@ -353,9 +353,9 @@ int memcmp(const void* s1, const void* s2, size_t n) {
   int size_s1;
   int size_s2;
   __require_allocated_array(s1);
-  size_s1 = __get_array_size(s1);
+  size_s1 = __get_array_length(s1);
   __require_allocated_array(s2);
-  size_s2 = __get_array_size(s2);
+  size_s2 = __get_array_length(s2);
   INFER_EXCLUDE_CONDITION((n > size_s1) || (n > size_s2));
   return __infer_nondet_int();
 }
@@ -368,9 +368,9 @@ void* memcpy(void* s1, const void* s2, size_t n) {
   __infer_set_flag("ignore_return",
                    ""); // no warnings if the return value is ignored
   __require_allocated_array(s1);
-  size_s1 = __get_array_size(s1);
+  size_s1 = __get_array_length(s1);
   __require_allocated_array(s2);
-  size_s2 = __get_array_size(s2);
+  size_s2 = __get_array_length(s2);
   INFER_EXCLUDE_CONDITION((n < 0) || (n > size_s1) || (n > size_s2));
   return s1;
 }
@@ -389,7 +389,7 @@ void* memset(void* s, int c, size_t n) {
   __infer_set_flag("ignore_return",
                    ""); // no warnings if the return value is ignored
   __require_allocated_array(s);
-  size_s = __get_array_size(s);
+  size_s = __get_array_length(s);
   INFER_EXCLUDE_CONDITION(n > size_s);
   return s;
 }
@@ -434,7 +434,7 @@ char* tmpnam(char* s) {
     return NULL;
   if (s) {
     __require_allocated_array(s);
-    size = __get_array_size(s);
+    size = __get_array_length(s);
     INFER_EXCLUDE_CONDITION(size < L_tmpnam);
     return s;
   } else
@@ -535,7 +535,7 @@ char* fgets(char* str, int num, FILE* stream) {
 
   if (n > 0) {
     __require_allocated_array(str);
-    size1 = __get_array_size(str);
+    size1 = __get_array_length(str);
     INFER_EXCLUDE_CONDITION(num > size1);
     return str;
   } else
@@ -614,7 +614,7 @@ char* getcwd(char* buffer, size_t size) {
 
   if (n > 0) {
     __require_allocated_array(buffer);
-    size_buf = __get_array_size(buffer);
+    size_buf = __get_array_length(buffer);
     INFER_EXCLUDE_CONDITION(size > size_buf);
     return buffer;
   } else
@@ -753,7 +753,7 @@ void* realloc(void* ptr, size_t size) {
   can_enlarge = __infer_nondet_int(); // nondeterministically choose whether the
   // current block can be enlarged
   if (can_enlarge) {
-    __set_array_size(ptr, size); // enlarge the block
+    __set_array_length(ptr, size); // enlarge the block
     return ptr;
   }
   int* newblock = (int*)malloc(size);
@@ -1167,7 +1167,7 @@ size_t strlcpy(char* dst, const char* src, size_t size) {
 
   // force dst to be allocated for at least size
   __require_allocated_array(dst);
-  size_dst = __get_array_size(dst);
+  size_dst = __get_array_length(dst);
   INFER_EXCLUDE_CONDITION(size > size_dst);
 
   INFER_EXCLUDE_CONDITION(res > size || res < 0);
@@ -1188,7 +1188,7 @@ size_t strlcat(char* dst, const char* src, size_t size) {
 
   // force dst to be allocated for at least size
   __require_allocated_array(dst);
-  size_dst = __get_array_size(dst);
+  size_dst = __get_array_length(dst);
   INFER_EXCLUDE_CONDITION(size > size_dst);
 
   INFER_EXCLUDE_CONDITION(res > size || res < 0);
@@ -1533,7 +1533,7 @@ ssize_t read(int fildes, void* buf, size_t nbyte) {
   if (nbyte == 0)
     return 0;
   __require_allocated_array(buf);
-  INFER_EXCLUDE_CONDITION(__get_array_size(buf) < nbyte);
+  INFER_EXCLUDE_CONDITION(__get_array_length(buf) < nbyte);
 
   int ret = __infer_nondet_int();
   INFER_EXCLUDE_CONDITION(ret < -1 || ret > nbyte);
@@ -1665,7 +1665,7 @@ size_t strcspn(const char* s1, const char* s2) {
 #if defined __APPLE__ || (defined __USE_XOPEN2K && !defined __USE_GNU)
 int strerror_r(int errnum, char* strerrbuf, size_t buflen) {
   __require_allocated_array(strerrbuf);
-  INFER_EXCLUDE_CONDITION(__get_array_size(strerrbuf) < buflen);
+  INFER_EXCLUDE_CONDITION(__get_array_length(strerrbuf) < buflen);
 
   return __infer_nondet_int();
 }
@@ -1673,7 +1673,7 @@ int strerror_r(int errnum, char* strerrbuf, size_t buflen) {
 
 ssize_t write(int fildes, const void* buf, size_t nbyte) {
   __require_allocated_array(buf);
-  INFER_EXCLUDE_CONDITION(__get_array_size(buf) < nbyte);
+  INFER_EXCLUDE_CONDITION(__get_array_length(buf) < nbyte);
 
   int ret = __infer_nondet_int();
   INFER_EXCLUDE_CONDITION(ret < -1 || nbyte < ret);
@@ -1731,7 +1731,7 @@ void* bsearch(const void* key,
   nondet = __infer_nondet_int();
   offset = __infer_nondet_int();
   __require_allocated_array(base);
-  base_size = __get_array_size(base);
+  base_size = __get_array_length(base);
   INFER_EXCLUDE_CONDITION(nmemb > base_size);
   if (nondet)
     return 0;
diff --git a/infer/models/c/src/wchar.c b/infer/models/c/src/wchar.c
index ebb8c32d2..8f5b3e64f 100644
--- a/infer/models/c/src/wchar.c
+++ b/infer/models/c/src/wchar.c
@@ -127,7 +127,7 @@ int CLIBCALL swprintf(wchar_t* restrict s,
                       ...) {
   int res;
   int size1;
-  size1 = __get_array_size(s);
+  size1 = __get_array_length(s);
   res = __infer_nondet_int();
   INFER_EXCLUDE_CONDITION(res < 0);
   return res;
diff --git a/infer/models/objc/src/CoreFoundation/CFString.c b/infer/models/objc/src/CoreFoundation/CFString.c
index 16a4dbf93..01d979c8d 100644
--- a/infer/models/objc/src/CoreFoundation/CFString.c
+++ b/infer/models/objc/src/CoreFoundation/CFString.c
@@ -12,7 +12,7 @@
 
 CFStringRef __cf_alloc(CFStringRef);
 
-void __get_array_size(const UInt8);
+void __get_array_length(const UInt8);
 
 CFStringRef CFStringCreateWithBytesNoCopy(CFAllocatorRef alloc,
                                           const UInt8* bytes,
@@ -24,7 +24,7 @@ CFStringRef CFStringCreateWithBytesNoCopy(CFAllocatorRef alloc,
   CFStringRef s = __cf_alloc(c);
   if (s) {
     if (bytes) {
-      __get_array_size(bytes);
+      __get_array_length(bytes);
       free(bytes);
     }
   }
diff --git a/infer/models/objc/src/NSString.m b/infer/models/objc/src/NSString.m
index ad7706407..2cc19a48c 100644
--- a/infer/models/objc/src/NSString.m
+++ b/infer/models/objc/src/NSString.m
@@ -10,7 +10,7 @@
 #import "NSString.h"
 #import <stdlib.h>
 
-void __get_array_size(const UInt8);
+void __get_array_length(const UInt8);
 
 @implementation NSString
 
@@ -41,7 +41,7 @@ void __get_array_size(const UInt8);
                        freeWhenDone:(BOOL)flag {
   if (flag == YES) {
     if (bytes) {
-      __get_array_size(bytes);
+      __get_array_length(bytes);
       free(bytes);
     }
   }
diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re
index e99fe8995..da4cbb4cb 100644
--- a/infer/src/IR/Sil.re
+++ b/infer/src/IR/Sil.re
@@ -741,6 +741,10 @@ and struct_typ = {
   def_methods: list Procname.t, /** methods defined */
   struct_annotations: item_annotation /** annotations */
 }
+/** statically determined length of an array type, if any */
+and static_length = option Int.t
+/** dynamically determined length of an array value, if any */
+and dynamic_length = option exp
 /** types for sil (structured) expressions */
 and typ =
   | Tvar of Typename.t /** named type */
@@ -750,7 +754,7 @@ and typ =
   | Tfun of bool /** function type with noreturn attribute */
   | Tptr of typ ptr_kind /** pointer type */
   | Tstruct of struct_typ /** Type for a structured value */
-  | Tarray of typ exp /** array type with fixed size */
+  | Tarray of typ static_length /** array type with statically fixed length */
 /** Program expressions. */
 and exp =
   /** Pure variable: it is not an lvalue */
@@ -769,10 +773,24 @@ and exp =
   | Lfield of exp Ident.fieldname typ
   /** An array index offset: [exp1\[exp2\]] */
   | Lindex of exp exp
-  /** 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;
+  /** A sizeof expression. [Sizeof (Tarray elt (Some static_length)) (Some dynamic_length)]
+      represents the size of an array value consisting of [dynamic_length] elements of type [elt].
+      The [dynamic_length], tracked by symbolic execution, may differ from the [static_length]
+      obtained from the type definition, e.g. when an array is over-allocated.  For struct types,
+      the [dynamic_length] is that of the final extensible array, if any. */
+  | Sizeof of typ dynamic_length Subtype.t;
+
+
+/** the element typ of the final extensible array in the given typ, if any */
+let rec get_extensible_array_element_typ =
+  fun
+  | Tarray typ _ => Some typ
+  | Tstruct {instance_fields} =>
+    Option.map_default
+      (fun (_, fld_typ, _) => get_extensible_array_element_typ fld_typ)
+      None
+      (IList.last instance_fields)
+  | _ => None;
 
 
 /** Kind of prune instruction */
@@ -873,10 +891,10 @@ type inst =
 type strexp =
   | Eexp of exp inst /** Base case: expression with instrumentation */
   | Estruct of (list (Ident.fieldname, strexp)) inst /** C structure */
-  | Earray of exp (list (exp, strexp)) inst /** Array of given size. */
+  | Earray of exp (list (exp, strexp)) inst /** Array of given length */
 /** There are two conditions imposed / used in the array case.
     First, if some index and value pair appears inside an array
-    in a strexp, then the index is less than the size of the array.
+    in a strexp, then the index is less than the length of the array.
     For instance, x |->[10 | e1: v1] implies that e1 <= 9.
     Second, if two indices appear in an array, they should be different.
     For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. */
@@ -2343,8 +2361,8 @@ and pp_struct_typ pe pp_base f struct_typ =>
   }
 /** Pretty print a type declaration.
     pp_base prints the variable for a declaration, or can be skip to print only the type
-    pp_size prints the expression for the array size */
-and pp_type_decl pe pp_base pp_size f =>
+    pp_static_len prints the expression for the array length */
+and pp_type_decl pe pp_base pp_static_len f =>
   fun
   | Tvar tname => F.fprintf f "%s %a" (Typename.to_string tname) pp_base ()
   | Tint ik => F.fprintf f "%s %a" (ikind_to_string ik) pp_base ()
@@ -2354,16 +2372,21 @@ and pp_type_decl pe pp_base pp_size f =>
   | Tfun true => F.fprintf f "_fn_noreturn_ %a" pp_base ()
   | Tptr ((Tarray _ | Tfun _) as typ) pk => {
       let pp_base' fmt () => F.fprintf fmt "(%s%a)" (ptr_kind_string pk) pp_base ();
-      pp_type_decl pe pp_base' pp_size f typ
+      pp_type_decl pe pp_base' pp_static_len f typ
     }
   | Tptr typ pk => {
       let pp_base' fmt () => F.fprintf fmt "%s%a" (ptr_kind_string pk) pp_base ();
-      pp_type_decl pe pp_base' pp_size f typ
+      pp_type_decl pe pp_base' pp_static_len f typ
     }
   | Tstruct struct_typ => pp_struct_typ pe pp_base f struct_typ
-  | Tarray typ size => {
-      let pp_base' fmt () => F.fprintf fmt "%a[%a]" pp_base () (pp_size pe) size;
-      pp_type_decl pe pp_base' pp_size f typ
+  | Tarray typ static_len => {
+      let pp_array_static_len fmt => (
+        fun
+        | Some static_len => pp_static_len pe fmt (Const (Cint static_len))
+        | None => F.fprintf fmt "_"
+      );
+      let pp_base' fmt () => F.fprintf fmt "%a[%a]" pp_base () pp_array_static_len static_len;
+      pp_type_decl pe pp_base' pp_static_len f typ
     }
 /** Pretty print a type with all the details, using the C syntax. */
 and pp_typ_full pe => pp_type_decl pe (fun _ () => ()) pp_exp_full
@@ -2994,10 +3017,9 @@ let rec pp_sexp_env pe0 envo f se => {
         F.fprintf f "%a:%a" (Ident.pp_fieldname_latex Latex.Boldface) n (pp_sexp_env pe envo) se;
       F.fprintf f "\\{%a\\}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst
     }
-  | Earray size nel inst =>
+  | Earray len nel inst =>
     let pp_diff f (i, se) => F.fprintf f "%a:%a" (pp_exp pe) i (pp_sexp_env pe envo) se;
-    F.fprintf
-      f "[%a|%a]%a" (pp_exp pe) size (pp_seq_diff pp_diff pe) nel (pp_inst_if_trace pe) inst
+    F.fprintf f "[%a|%a]%a" (pp_exp pe) len (pp_seq_diff pp_diff pe) nel (pp_inst_if_trace pe) inst
   };
   color_post_wrapper changed pe0 f
 }
@@ -3205,13 +3227,13 @@ let rec strexp_expmap (f: (exp, option inst) => (exp, option inst)) => {
       let f_fld_se (fld, se) => (fld, strexp_expmap f se);
       Estruct (IList.map f_fld_se fld_se_list) inst
     }
-  | Earray size idx_se_list inst => {
-      let size' = fe size;
+  | Earray len idx_se_list inst => {
+      let len' = fe len;
       let f_idx_se (idx, se) => {
         let idx' = fe idx;
         (idx', strexp_expmap f se)
       };
-      Earray size' (IList.map f_idx_se idx_se_list) inst
+      Earray len' (IList.map f_idx_se idx_se_list) inst
     }
 };
 
@@ -3246,9 +3268,9 @@ let rec strexp_instmap (f: inst => inst) strexp =>
   | Estruct fld_se_list inst =>
     let f_fld_se (fld, se) => (fld, strexp_instmap f se);
     Estruct (IList.map f_fld_se fld_se_list) (f inst)
-  | Earray size idx_se_list inst =>
+  | Earray len idx_se_list inst =>
     let f_idx_se (idx, se) => (idx, strexp_instmap f se);
-    Earray size (IList.map f_idx_se idx_se_list) (f inst)
+    Earray len (IList.map f_idx_se idx_se_list) (f inst)
   }
 and hpara_instmap (f: inst => inst) hpara => {
   ...hpara,
@@ -3449,10 +3471,10 @@ let rec strexp_fpv =
       let f (_, se) => strexp_fpv se;
       IList.flatten (IList.map f fld_se_list)
     }
-  | Earray size idx_se_list _ => {
-      let fpv_in_size = exp_fpv size;
+  | Earray len idx_se_list _ => {
+      let fpv_in_len = exp_fpv len;
       let f (idx, se) => exp_fpv idx @ strexp_fpv se;
-      fpv_in_size @ IList.flatten (IList.map f idx_se_list)
+      fpv_in_len @ IList.flatten (IList.map f idx_se_list)
     }
 and hpred_fpv =
   fun
@@ -3662,8 +3684,8 @@ let rec strexp_fav_add fav =>
   fun
   | Eexp e _ => exp_fav_add fav e
   | Estruct fld_se_list _ => IList.iter (fun (_, se) => strexp_fav_add fav se) fld_se_list
-  | Earray size idx_se_list _ => {
-      exp_fav_add fav size;
+  | Earray len idx_se_list _ => {
+      exp_fav_add fav len;
       IList.iter
         (
           fun (e, se) => {
@@ -4015,18 +4037,7 @@ let sub_fpv (sub: subst) => IList.flatten (IList.map (fun (_, e) => exp_fpv e) s
 /** Substitutions do not contain binders */
 let sub_av_add = sub_fav_add;
 
-let rec typ_sub (subst: subst) typ =>
-  switch typ {
-  | Tvar _
-  | Tint _
-  | Tfloat _
-  | Tvoid
-  | Tstruct _
-  | Tfun _ => typ
-  | Tptr t' pk => Tptr (typ_sub subst t') pk
-  | Tarray t e => Tarray (typ_sub subst t) (exp_sub subst e)
-  }
-and exp_sub (subst: subst) e =>
+let rec exp_sub (subst: subst) e =>
   switch e {
   | Var id =>
     let rec apply_sub = (
@@ -4053,12 +4064,7 @@ and exp_sub (subst: subst) e =>
     Cast t e1'
   | UnOp op e1 typo =>
     let e1' = exp_sub subst e1;
-    let typo' =
-      switch typo {
-      | None => None
-      | Some typ => Some (typ_sub subst typ)
-      };
-    UnOp op e1' typo'
+    UnOp op e1' typo
   | BinOp op e1 e2 =>
     let e1' = exp_sub subst e1;
     let e2' = exp_sub subst e2;
@@ -4066,13 +4072,12 @@ and exp_sub (subst: subst) e =>
   | Lvar _ => e
   | Lfield e1 fld typ =>
     let e1' = exp_sub subst e1;
-    let typ' = typ_sub subst typ;
-    Lfield e1' fld typ'
+    Lfield e1' fld typ
   | Lindex e1 e2 =>
     let e1' = exp_sub subst e1;
     let e2' = exp_sub subst e2;
     Lindex e1' e2'
-  | Sizeof t l s => Sizeof (typ_sub subst t) (Option.map (exp_sub subst) l) s
+  | Sizeof t l s => Sizeof t (Option.map (exp_sub subst) l) s
   };
 
 let instr_sub (subst: subst) instr => {
@@ -4082,20 +4087,19 @@ let instr_sub (subst: subst) instr => {
     | _ => id
     };
   let exp_s = exp_sub subst;
-  let typ_s = typ_sub subst;
   switch instr {
-  | Letderef id e t loc => Letderef (id_s id) (exp_s e) (typ_s t) loc
-  | Set e1 t e2 loc => Set (exp_s e1) (typ_s t) (exp_s e2) loc
+  | Letderef id e t loc => Letderef (id_s id) (exp_s e) t loc
+  | Set e1 t e2 loc => Set (exp_s e1) t (exp_s e2) loc
   | Prune cond loc true_branch ik => Prune (exp_s cond) loc true_branch ik
   | Call ret_ids e arg_ts loc cf =>
-    let arg_s (e, t) => (exp_s e, typ_s t);
+    let arg_s (e, t) => (exp_s e, t);
     Call (IList.map id_s ret_ids) (exp_s e) (IList.map arg_s arg_ts) loc cf
   | Nullify _ => instr
   | Abstract _ => instr
   | Remove_temps temps loc => Remove_temps (IList.map id_s temps) loc
   | Stackop _ => instr
   | Declare_locals ptl loc =>
-    let pt_s (pv, t) => (pv, typ_s t);
+    let pt_s (pv, t) => (pv, t);
     Declare_locals (IList.map pt_s ptl) loc
   }
 };
@@ -4512,13 +4516,13 @@ let rec strexp_replace_exp epairs =>
       let f (fld, se) => (fld, strexp_replace_exp epairs se);
       Estruct (IList.map f fsel) inst
     }
-  | Earray size isel inst => {
-      let size' = exp_replace_exp epairs size;
+  | Earray len isel inst => {
+      let len' = exp_replace_exp epairs len;
       let f (idx, se) => {
         let idx' = exp_replace_exp epairs idx;
         (idx', strexp_replace_exp epairs se)
       };
-      Earray size' (IList.map f isel) inst
+      Earray len' (IList.map f isel) inst
     };
 
 let hpred_replace_exp epairs =>
diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei
index c4ec13d71..ecef79342 100644
--- a/infer/src/IR/Sil.rei
+++ b/infer/src/IR/Sil.rei
@@ -314,6 +314,10 @@ and struct_typ = {
   def_methods: list Procname.t, /** methods defined */
   struct_annotations: item_annotation /** annotations */
 }
+/** statically determined length of an array type, if any */
+and static_length = option Int.t
+/** dynamically determined length of an array value, if any */
+and dynamic_length = option exp
 /** Types for sil (structured) expressions. */
 and typ =
   | Tvar of Typename.t /** named type */
@@ -323,7 +327,7 @@ and typ =
   | Tfun of bool /** function type with noreturn attribute */
   | Tptr of typ ptr_kind /** pointer type */
   | Tstruct of struct_typ /** Type for a structured value */
-  | Tarray of typ exp /** array type with fixed size */
+  | Tarray of typ static_length /** array type with statically fixed length */
 /** Program expressions. */
 and exp =
   /** Pure variable: it is not an lvalue */
@@ -342,8 +346,14 @@ and exp =
   | Lfield of exp Ident.fieldname typ
   /** An array index offset: [exp1\[exp2\]] */
   | Lindex of exp exp
-  /** A sizeof expression */
-  | Sizeof of typ (option exp) 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 length in [Tarray] records the
+      statically determined length, while the length in [Sizeof] records the dynamic length. */
+  | Sizeof of typ dynamic_length Subtype.t;
+
+
+/** the element typ of the final extensible array in the given typ, if any */
+let get_extensible_array_element_typ: typ => option typ;
 
 let struct_typ_equal: struct_typ => struct_typ => bool;
 
@@ -528,10 +538,10 @@ let inst_partial_meet: inst => inst => inst;
 type strexp =
   | Eexp of exp inst /** Base case: expression with instrumentation */
   | Estruct of (list (Ident.fieldname, strexp)) inst /** C structure */
-  | Earray of exp (list (exp, strexp)) inst /** Array of given size. */
+  | Earray of exp (list (exp, strexp)) inst /** Array of given length */
 /** There are two conditions imposed / used in the array case.
     First, if some index and value pair appears inside an array
-    in a strexp, then the index is less than the size of the array.
+    in a strexp, then the index is less than the length of the array.
     For instance, x |->[10 | e1: v1] implies that e1 <= 9.
     Second, if two indices appear in an array, they should be different.
     For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. */
@@ -886,9 +896,9 @@ let pp_typ_full: printenv => F.formatter => typ => unit;
 let typ_to_string: typ => string;
 
 
-/** [pp_type_decl pe pp_base pp_size f typ] pretty prints a type declaration.
+/** [pp_type_decl pe pp_base pp_len f typ] pretty prints a type declaration.
     pp_base prints the variable for a declaration, or can be skip to print only the type
-    pp_size prints the expression for the array size */
+    pp_len prints the expression for the array length */
 let pp_type_decl:
   printenv =>
   (F.formatter => unit => unit) =>
diff --git a/infer/src/IR/Tenv.re b/infer/src/IR/Tenv.re
index c3bada373..a47488ce6 100644
--- a/infer/src/IR/Tenv.re
+++ b/infer/src/IR/Tenv.re
@@ -57,9 +57,8 @@ let lookup_java_typ_from_string tenv typ_str => {
     | "double" => Some (Sil.Tfloat Sil.FDouble)
     | typ_str when String.contains typ_str '[' => {
         let stripped_typ = String.sub typ_str 0 (String.length typ_str - 2);
-        let array_typ_size = Sil.exp_get_undefined false;
         switch (loop stripped_typ) {
-        | Some typ => Some (Sil.Tptr (Sil.Tarray typ array_typ_size) Sil.Pk_pointer)
+        | Some typ => Some (Sil.Tptr (Sil.Tarray typ None) Sil.Pk_pointer)
         | None => None
         }
       }
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index a1af433cc..e9a63edd5 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -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
@@ -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 =
diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml
index 904a90bf6..f274cbebf 100644
--- a/infer/src/backend/absarray.ml
+++ b/infer/src/backend/absarray.ml
@@ -28,7 +28,7 @@ module StrexpMatch : sig
   (** create a path from a root and a list of offsets *)
   val path_from_exp_offsets : Sil.exp -> Sil.offset list -> path
 
-  (** path to the root, size, elements and type of a new_array *)
+  (** path to the root, length, elements and type of a new_array *)
   type strexp_data = path * Sil.strexp * Sil.typ
 
   (** sigma with info about a current array *)
@@ -73,7 +73,7 @@ end = struct
             (IList.find (fun (f', _, _) ->
                  Sil.fld_equal f' fld) instance_fields) in
         get_strexp_at_syn_offsets se' t' syn_offs'
-    | Sil.Earray (_, esel, _), Sil.Tarray(t', _), Index ind :: syn_offs' ->
+    | Sil.Earray (_, esel, _), Sil.Tarray (t', _), Index ind :: syn_offs' ->
         let se' = snd (IList.find (fun (i', _) -> Sil.exp_equal i' ind) esel) in
         get_strexp_at_syn_offsets se' t' syn_offs'
     | _ ->
@@ -95,11 +95,11 @@ end = struct
         let se_mod = replace_strexp_at_syn_offsets se' t' syn_offs' update in
         let fsel' = IList.map (fun (f'', se'') -> if Sil.fld_equal f'' fld then (fld, se_mod) else (f'', se'')) fsel in
         Sil.Estruct (fsel', inst)
-    | Sil.Earray (size, esel, inst), Sil.Tarray (t', _), Index idx :: syn_offs' ->
+    | Sil.Earray (len, esel, inst), Sil.Tarray (t', _), Index idx :: syn_offs' ->
         let se' = snd (IList.find (fun (i', _) -> Sil.exp_equal i' idx) esel) in
         let se_mod = replace_strexp_at_syn_offsets se' t' syn_offs' update in
         let esel' = IList.map (fun ese -> if Sil.exp_equal (fst ese) idx then (idx, se_mod) else ese) esel in
-        Sil.Earray (size, esel', inst)
+        Sil.Earray (len, esel', inst)
     | _ -> assert false
 
   (** convert a path into an expression *)
@@ -124,7 +124,7 @@ end = struct
     let syn_offs = IList.map offset_to_syn_offset offs in
     (root, syn_offs)
 
-  (** path to the root, size, elements and type of a new_array *)
+  (** path to the root, len, elements and type of a new_array *)
   type strexp_data = path * Sil.strexp * Sil.typ
 
   (** Store hpred using physical equality, and offset list for an array *)
@@ -205,13 +205,13 @@ end = struct
     let update se' =
       let se_in = update se' in
       match se', se_in with
-      | Sil.Earray (size, esel, _), Sil.Earray (_, esel_in, inst2) ->
+      | Sil.Earray (len, esel, _), Sil.Earray (_, esel_in, inst2) ->
           let orig_indices = IList.map fst esel in
           let index_is_not_new idx = IList.exists (Sil.exp_equal idx) orig_indices in
           let process_index idx =
             if index_is_not_new idx then idx else (Sil.array_clean_new_index footprint_part idx) in
           let esel_in' = IList.map (fun (idx, se) -> process_index idx, se) esel_in in
-          Sil.Earray (size, esel_in', inst2)
+          Sil.Earray (len, esel_in', inst2)
       | _, _ -> se_in in
     begin
       match hpred with
@@ -232,9 +232,9 @@ end = struct
   let replace_index footprint_part ((sigma, hpred, syn_offs) : t) (index: Sil.exp) (index': Sil.exp) =
     let update se' =
       match se' with
-      | Sil.Earray (size, esel, inst) ->
+      | Sil.Earray (len, esel, inst) ->
           let esel' = IList.map (fun (e', se') -> if Sil.exp_equal e' index then (index', se') else (e', se')) esel in
-          Sil.Earray (size, esel', inst)
+          Sil.Earray (len, esel', inst)
       | _ -> assert false in
     let hpred' = hpred_replace_strexp footprint_part hpred syn_offs update in
     replace_hpred (sigma, hpred, syn_offs) hpred'
@@ -413,11 +413,11 @@ let keep_only_indices
       let matched = StrexpMatch.find_path sigma path in
       let (_, se, _) = StrexpMatch.get_data matched in
       match se with
-      | Sil.Earray (size, esel, inst) ->
+      | Sil.Earray (len, esel, inst) ->
           let esel', esel_leftover' = IList.partition (fun (e, _) -> IList.exists (Sil.exp_equal e) indices) esel in
           if esel_leftover' == [] then (sigma, false)
           else begin
-            let se' = Sil.Earray (size, esel', inst) in
+            let se' = Sil.Earray (len, esel', inst) in
             let sigma' = StrexpMatch.replace_strexp footprint_part matched se' in
             (sigma', true)
           end
@@ -584,9 +584,9 @@ let remove_redundant_elements prop =
         remove () (* index unknown can be removed *)
     | _ -> true in
   let remove_redundant_se fp_part = function
-    | Sil.Earray (size, esel, inst) ->
+    | Sil.Earray (len, esel, inst) ->
         let esel' = IList.filter (filter_redundant_e_se fp_part) esel in
-        Sil.Earray (size, esel', inst)
+        Sil.Earray (len, esel', inst)
     | se -> se in
   let remove_redundant_hpred fp_part = function
     | Sil.Hpointsto (e, se, te) ->
diff --git a/infer/src/backend/autounit.ml b/infer/src/backend/autounit.ml
index 7fb99f361..6f4b19133 100644
--- a/infer/src/backend/autounit.ml
+++ b/infer/src/backend/autounit.ml
@@ -307,8 +307,8 @@ let create_idmap sigma : idmap =
         do_exp e typ
     | Sil.Estruct (fsel, _), Sil.Tstruct { Sil.instance_fields } ->
         do_struct fsel instance_fields
-    | Sil.Earray (size, esel, _), Sil.Tarray (typ, _) ->
-        do_se (Sil.Eexp (size, Sil.inst_none)) (Sil.Tint Sil.IULong);
+    | Sil.Earray (len, esel, _), Sil.Tarray (typ, _) ->
+        do_se (Sil.Eexp (len, Sil.inst_none)) (Sil.Tint Sil.IULong);
         do_array esel typ
     | _ ->
         L.err "Unmatched sexp: %a : %a@." (Sil.pp_sexp pe) se (Sil.pp_typ_full pe) typ;
@@ -415,20 +415,20 @@ let mk_size_name id =
   "_size_" ^ string_of_int id
 
 let pp_texp_for_malloc fmt =
-  let rec handle_arr_size typ = match typ with
+  let rec handle_arr_len typ = match typ with
     | Sil.Tvar _ | Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ ->
         typ
     | Sil.Tptr (t, pk) ->
-        Sil.Tptr (handle_arr_size t, pk)
+        Sil.Tptr (handle_arr_len t, pk)
     | Sil.Tstruct struct_typ ->
         let instance_fields =
-          IList.map (fun (f, t, a) -> (f, handle_arr_size t, a)) struct_typ.Sil.instance_fields in
+          IList.map (fun (f, t, a) -> (f, handle_arr_len t, a)) struct_typ.Sil.instance_fields in
         Sil.Tstruct { struct_typ with Sil.instance_fields }
     | Sil.Tarray (t, e) ->
-        Sil.Tarray (handle_arr_size t, e) in
+        Sil.Tarray (handle_arr_len t, e) in
   function
   | Sil.Sizeof (typ, _, _) ->
-      let typ' = handle_arr_size typ in
+      let typ' = handle_arr_len 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 c4d9f300f..e3c2d625d 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -877,6 +877,12 @@ let ident_partial_meet (id1: Ident.t) (id2: Ident.t) =
 
 (** {2 Join and Meet for Exps} *)
 
+let option_partial_join partial_join o1 o2 =
+  match o1, o2 with
+  | None, _ -> o2
+  | _, None -> o1
+  | 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
@@ -951,35 +957,36 @@ let rec exp_partial_join (e1: Sil.exp) (e2: Sil.exp) : Sil.exp =
       let e2'' = exp_partial_join e1' e2' in
       Sil.Lindex(e1'', e2'')
   | 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)
+      Sil.Sizeof
+        (typ_partial_join t1 t2, dynamic_length_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
+and length_partial_join len1 len2 = match len1, len2 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
       let c' = exp_partial_join (Sil.Const c1) (Sil.Const c2) in
       Sil.BinOp (Sil.PlusA, e', c')
   | Sil.BinOp(Sil.PlusA, _, _), Sil.BinOp(Sil.PlusA, _, _) ->
-      Rename.extend size1 size2 Rename.ExtFresh
+      Rename.extend len1 len2 Rename.ExtFresh
   | Sil.Var id1, Sil.Var id2 when Ident.equal id1 id2 ->
-      size1
-  | _ -> exp_partial_join size1 size2
+      len1
+  | _ -> exp_partial_join len1 len2
+
+and static_length_partial_join l1 l2 =
+  option_partial_join (fun len1 len2 -> if Sil.Int.eq len1 len2 then Some len1 else None) l1 l2
+
+and dynamic_length_partial_join l1 l2 =
+  option_partial_join (fun len1 len2 -> Some (length_partial_join len1 len2)) l1 l2
 
 and typ_partial_join t1 t2 = match t1, t2 with
   | Sil.Tptr (t1, pk1), Sil.Tptr (t2, pk2) when Sil.ptr_kind_compare pk1 pk2 = 0 ->
       Sil.Tptr (typ_partial_join t1 t2, pk1)
-  | Sil.Tarray (typ1, size1), Sil.Tarray(typ2, size2) ->
+  | Sil.Tarray (typ1, len1), Sil.Tarray (typ2, len2) ->
       let t = typ_partial_join typ1 typ2 in
-      let size = size_partial_join size1 size2 in
-      Sil.Tarray (t, size)
+      let len = static_length_partial_join len1 len2 in
+      Sil.Tarray (t, len)
   | _ when Sil.typ_equal t1 t2 -> t1 (* common case *)
   | _ ->
       L.d_str "typ_partial_join no match "; Sil.d_typ_full t1; L.d_str " "; Sil.d_typ_full t2; L.d_ln ();
@@ -1072,21 +1079,21 @@ let rec strexp_partial_join mode (strexp1: Sil.strexp) (strexp2: Sil.strexp) : S
                 assert false (* This case should not happen. *)
         end in
 
-  let rec f_idx_se_list inst size idx_se_list_acc idx_se_list1 idx_se_list2 =
+  let rec f_idx_se_list inst len idx_se_list_acc idx_se_list1 idx_se_list2 =
     match idx_se_list1, idx_se_list2 with
-    | [], [] -> Sil.Earray (size, IList.rev idx_se_list_acc, inst)
+    | [], [] -> Sil.Earray (len, IList.rev idx_se_list_acc, inst)
     | [], _ | _, [] ->
         begin
           match mode with
           | JoinState.Pre -> (L.d_strln "failure reason 44"; raise IList.Fail)
           | JoinState.Post ->
-              Sil.Earray (size, IList.rev idx_se_list_acc, inst)
+              Sil.Earray (len, IList.rev idx_se_list_acc, inst)
         end
     | (idx1, se1):: idx_se_list1', (idx2, se2):: idx_se_list2' ->
         let idx = exp_partial_join idx1 idx2 in
         let strexp' = strexp_partial_join mode se1 se2 in
         let idx_se_list_new = (idx, strexp') :: idx_se_list_acc in
-        f_idx_se_list inst size idx_se_list_new idx_se_list1' idx_se_list2' in
+        f_idx_se_list inst len idx_se_list_new idx_se_list1' idx_se_list2' in
 
   match strexp1, strexp2 with
   | Sil.Eexp (e1, inst1), Sil.Eexp (e2, inst2) ->
@@ -1094,10 +1101,10 @@ let rec strexp_partial_join mode (strexp1: Sil.strexp) (strexp2: Sil.strexp) : S
   | Sil.Estruct (fld_se_list1, inst1), Sil.Estruct (fld_se_list2, inst2) ->
       let inst = Sil.inst_partial_join inst1 inst2 in
       f_fld_se_list inst mode [] fld_se_list1 fld_se_list2
-  | Sil.Earray (size1, idx_se_list1, inst1), Sil.Earray (size2, idx_se_list2, inst2) ->
-      let size = size_partial_join size1 size2 in
+  | Sil.Earray (len1, idx_se_list1, inst1), Sil.Earray (len2, idx_se_list2, inst2) ->
+      let len = length_partial_join len1 len2 in
       let inst = Sil.inst_partial_join inst1 inst2 in
-      f_idx_se_list inst size [] idx_se_list1 idx_se_list2
+      f_idx_se_list inst len [] idx_se_list1 idx_se_list2
   | _ -> L.d_strln "no match in strexp_partial_join"; raise IList.Fail
 
 let rec strexp_partial_meet (strexp1: Sil.strexp) (strexp2: Sil.strexp) : Sil.strexp =
@@ -1130,19 +1137,19 @@ let rec strexp_partial_meet (strexp1: Sil.strexp) (strexp2: Sil.strexp) : Sil.st
           let acc_new = (fld1, strexp') :: acc in
           f_fld_se_list inst acc_new fld_se_list1' fld_se_list2' in
 
-  let rec f_idx_se_list inst size acc idx_se_list1 idx_se_list2 =
+  let rec f_idx_se_list inst len acc idx_se_list1 idx_se_list2 =
     match idx_se_list1, idx_se_list2 with
     | [],[] ->
-        Sil.Earray (size, IList.rev acc, inst)
+        Sil.Earray (len, IList.rev acc, inst)
     | [], _ ->
-        Sil.Earray (size, construct Rhs acc idx_se_list2, inst)
+        Sil.Earray (len, construct Rhs acc idx_se_list2, inst)
     | _, [] ->
-        Sil.Earray (size, construct Lhs acc idx_se_list1, inst)
+        Sil.Earray (len, construct Lhs acc idx_se_list1, inst)
     | (idx1, se1):: idx_se_list1', (idx2, se2):: idx_se_list2' ->
         let idx = exp_partial_meet idx1 idx2 in
         let se' = strexp_partial_meet se1 se2 in
         let acc_new = (idx, se') :: acc in
-        f_idx_se_list inst size acc_new idx_se_list1' idx_se_list2' in
+        f_idx_se_list inst len acc_new idx_se_list1' idx_se_list2' in
 
   match strexp1, strexp2 with
   | Sil.Eexp (e1, inst1), Sil.Eexp (e2, inst2) ->
@@ -1150,10 +1157,10 @@ let rec strexp_partial_meet (strexp1: Sil.strexp) (strexp2: Sil.strexp) : Sil.st
   | Sil.Estruct (fld_se_list1, inst1), Sil.Estruct (fld_se_list2, inst2) ->
       let inst = Sil.inst_partial_meet inst1 inst2 in
       f_fld_se_list inst [] fld_se_list1 fld_se_list2
-  | Sil.Earray (size1, idx_se_list1, inst1), Sil.Earray (size2, idx_se_list2, inst2)
-    when Sil.exp_equal size1 size2 ->
+  | Sil.Earray (len1, idx_se_list1, inst1), Sil.Earray (len2, idx_se_list2, inst2)
+    when Sil.exp_equal len1 len2 ->
       let inst = Sil.inst_partial_meet inst1 inst2 in
-      f_idx_se_list inst size1 [] idx_se_list1 idx_se_list2
+      f_idx_se_list inst len1 [] idx_se_list1 idx_se_list2
   | _ -> (L.d_strln "failure reason 52"; raise IList.Fail)
 
 (** {2 Join and Meet for kind, hpara, hpara_dll} *)
@@ -1554,26 +1561,26 @@ let pi_partial_join mode
     | Sil.Const _ -> true
     (* | Sil.Lvar _ -> true *)
     | _ -> false in
-  let get_array_size prop =
-    (* find some array size in the prop, to be used as heuritic for upper bound in widening *)
-    let size_list = ref [] in
+  let get_array_len prop =
+    (* 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), _, _), _) ->
-          (if Sil.Int.geq n Sil.Int.one then size_list := n::!size_list)
+          (if Sil.Int.geq n Sil.Int.one then len_list := n :: !len_list)
       | _ -> () in
     IList.iter do_hpred (Prop.get_sigma prop);
-    !size_list in
+    !len_list in
   let bounds =
-    let bounds1 = get_array_size ep1 in
-    let bounds2 = get_array_size ep2 in
+    let bounds1 = get_array_len ep1 in
+    let bounds2 = get_array_len ep2 in
     let bounds_sorted = IList.sort Sil.Int.compare_value (bounds1@bounds2) in
     IList.rev (IList.remove_duplicates Sil.Int.compare_value bounds_sorted) in
   let widening_atom a =
-    (* widening heuristic for upper bound: take the size of some array, -2 and -1 *)
+    (* widening heuristic for upper bound: take the length of some array, -2 and -1 *)
     match Prop.atom_exp_le_const a, bounds with
-    | Some (e, n), size:: _ ->
-        let first_try = Sil.Int.sub size Sil.Int.one in
-        let second_try = Sil.Int.sub size Sil.Int.two in
+    | Some (e, n), len :: _ ->
+        let first_try = Sil.Int.sub len Sil.Int.one in
+        let second_try = Sil.Int.sub len Sil.Int.two in
         let bound =
           if Sil.Int.leq n first_try then
             if Sil.Int.leq n second_try then second_try else first_try
@@ -1629,14 +1636,14 @@ let pi_partial_join mode
           | Some (e, n) ->
               if IList.exists (is_stronger_le e n) pi_op then (widening_atom a_res) else Some a_res
         end in
-  let handle_atom_with_widening size p_op pi_op atom_list a =
+  let handle_atom_with_widening len p_op pi_op atom_list a =
     (* find a join for the atom, if it fails apply widening heuristing and try again *)
-    match join_atom size p_op pi_op a with
+    match join_atom len p_op pi_op a with
     | None ->
         (match widening_atom a with
          | None -> atom_list
          | Some a' ->
-             (match join_atom size p_op pi_op a' with
+             (match join_atom len p_op pi_op a' with
               | None -> atom_list
               | Some a' -> a' :: atom_list))
     | Some a' -> a' :: atom_list in
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index 3e45a9bb3..af548c053 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -65,7 +65,7 @@ type dotty_node =
   (* Dotstruct(coo,e,l,c): struct box for expression e  with field list l at coordinate coo and color c *)
   | Dotstruct of coordinate * Sil.exp * (Ident.fieldname * Sil.strexp) list * string * Sil.exp
   (* Dotarray(coo,e1,e2,l,t,c): array box for expression e1  with field list l at coordinate coo and color c*)
-  (* e2 is the size and t is the type *)
+  (* e2 is the len and t is the type *)
   | Dotarray of coordinate * Sil.exp * Sil.exp * (Sil.exp * Sil.strexp) list * Sil.typ * string
   (* Dotlseg(coo,e1,e2,k,h,c): list box from e1 to e2 at coordinate coo and color c*)
   | Dotlseg of coordinate * Sil.exp * Sil.exp * Sil.lseg_kind * Sil.hpred list * string
@@ -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
@@ -1221,13 +1221,13 @@ let rec compute_target_nodes_from_sexp nodes se prop field_lab =
            compute_target_nodes_from_sexp nodes se2 prop (Ident.fieldname_to_string fn) @
            compute_target_nodes_from_sexp nodes (Sil.Estruct (l', inst)) prop ""
       )
-  | Sil.Earray(size, lie, inst) ->
+  | Sil.Earray (len, lie, inst) ->
       (match lie with
        | [] -> []
        | (idx, se2):: l' ->
            let lab ="["^exp_to_xml_string idx^"]" in
            compute_target_nodes_from_sexp nodes se2 prop lab @
-           compute_target_nodes_from_sexp nodes (Sil.Earray(size, l', inst)) prop ""
+           compute_target_nodes_from_sexp nodes (Sil.Earray (len, l', inst)) prop ""
       )
 
 
@@ -1291,9 +1291,9 @@ let rec pointsto_contents_to_xml (co: Sil.strexp) : Io_infer.Xml.node =
   | Sil.Estruct (fel, _) ->
       let f (fld, exp) = Io_infer.Xml.create_tree "struct-field" [("id", Ident.fieldname_to_string fld)] [(pointsto_contents_to_xml exp)] in
       Io_infer.Xml.create_tree "struct" [] (IList.map f fel)
-  | Sil.Earray (size, nel, _) ->
+  | Sil.Earray (len, nel, _) ->
       let f (e, se) = Io_infer.Xml.create_tree "array-element" [("index", exp_to_xml_string e)] [pointsto_contents_to_xml se] in
-      Io_infer.Xml.create_tree "array" [("size", exp_to_xml_string size)] (IList.map f nel)
+      Io_infer.Xml.create_tree "array" [("size", exp_to_xml_string len)] (IList.map f nel)
 
 (* Convert an atom to xml in a light version. Namely, the expressions are not fully blown-up into *)
 (* xml tree but visualized as strings *)
diff --git a/infer/src/backend/iList.ml b/infer/src/backend/iList.ml
index c9b8e8bc9..0c4ddbca9 100644
--- a/infer/src/backend/iList.ml
+++ b/infer/src/backend/iList.ml
@@ -29,8 +29,8 @@ let stable_sort = List.stable_sort
 let tl = List.tl
 
 let rec last = function
-  | [] -> invalid_arg "IList.last"
-  | [x] -> x
+  | [] -> None
+  | [x] -> Some x
   | _ :: xs -> last xs
 
 (** tail-recursive variant of List.fold_right *)
diff --git a/infer/src/backend/iList.mli b/infer/src/backend/iList.mli
index c2a241d75..b054cd329 100644
--- a/infer/src/backend/iList.mli
+++ b/infer/src/backend/iList.mli
@@ -64,8 +64,8 @@ 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
+(** last element, if any *)
+val last : 'a list -> 'a option
 
 (* Drops the first n elements from a list. *)
 val drop_first : int -> 'a list -> 'a list
diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml
index 3b8b4b688..08b0545cb 100644
--- a/infer/src/backend/match.ml
+++ b/infer/src/backend/match.ml
@@ -101,8 +101,8 @@ let rec strexp_match sexp1 sub vars sexp2 : (Sil.subst * Ident.t list) option =
       fsel_match fsel1 sub vars fsel2
   | Sil.Estruct _, _ | _, Sil.Estruct _ ->
       None
-  | Sil.Earray (size1, isel1, _), Sil.Earray (size2, isel2, _) ->
-      (match exp_match size1 sub vars size2 with
+  | Sil.Earray (len1, isel1, _), Sil.Earray (len2, isel2, _) ->
+      (match exp_match len1 sub vars len2 with
        | Some (sub', vars') -> isel_match isel1 sub' vars' isel2
        | None -> None)
 
@@ -497,8 +497,8 @@ let rec generate_todos_from_strexp mode todos sexp1 sexp2 =
       else generate_todos_from_fel mode todos fel1 fel2
   | Sil.Estruct _, _ ->
       None
-  | Sil.Earray (size1, iel1, _), Sil.Earray (size2, iel2, _) ->
-      if (not (Sil.exp_equal size1 size2) || IList.length iel1 <> IList.length iel2)
+  | Sil.Earray (len1, iel1, _), Sil.Earray (len2, iel2, _) ->
+      if (not (Sil.exp_equal len1 len2) || IList.length iel1 <> IList.length iel2)
       then None
       else generate_todos_from_iel mode todos iel1 iel2
   | Sil.Earray _, _ ->
diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml
index 55bc82eac..f53fbd29f 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/modelBuiltins.ml
@@ -28,24 +28,24 @@ let execute___builtin_va_arg { Builtin.pdesc; tenv; prop_; path; ret_ids; args;
       SymExec.instrs ~mask_errors:true tenv pdesc [instr'] [(prop_, path)]
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
-let mk_empty_array size =
-  Sil.Earray (size, [], Sil.inst_none)
+let mk_empty_array len =
+  Sil.Earray (len, [], Sil.inst_none)
 
 (* Make a rearranged array. As it is rearranged when it appears in a precondition
    it requires that the function is called with the array allocated. If not infer
    return a null pointer deref *)
-let mk_empty_array_rearranged size =
-  Sil.Earray (size, [], Sil.inst_rearrange true (State.get_loc ()) (State.get_path_pos ()))
+let mk_empty_array_rearranged len =
+  Sil.Earray (len, [], Sil.inst_rearrange true (State.get_loc ()) (State.get_path_pos ()))
 
 let extract_array_type typ =
   if (!Config.curr_language = Config.Java) then
     match typ with
-    | Sil.Tptr ( Sil.Tarray (typ', _), _) -> Some typ'
+    | Sil.Tptr (Sil.Tarray _ as arr, _) -> Some arr
     | _ -> None
   else
     match typ with
-    | Sil.Tptr (typ', _) | Sil.Tarray (typ', _) ->
-        Some typ'
+    | Sil.Tarray _ as arr -> Some arr
+    | Sil.Tptr (elt, _) -> Some (Sil.Tarray (elt, None))
     | _ -> None
 
 (** Return a result from a procedure call. *)
@@ -54,8 +54,8 @@ let return_result e prop ret_ids =
   | [ret_id] -> Prop.conjoin_eq e (Sil.Var ret_id) prop
   | _ -> prop
 
-(* Add an array of typ pointed to by lexp to prop_ if it doesnt exist alread*)
-(*  Return the new prop and the array size *)
+(* Add an array of typ pointed to by lexp to prop_ if it doesn't already exist *)
+(*  Return the new prop and the array length *)
 (*  Return None if it fails to add the array *)
 let add_array_to_prop pdesc prop_ lexp typ =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
@@ -66,24 +66,21 @@ let add_array_to_prop pdesc prop_ lexp typ =
           | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
           | _ -> false) (Prop.get_sigma prop) in
       match hpred with
-      | Sil.Hpointsto(_, Sil.Earray(size, _, _), _) ->
-          Some (size, prop)
+      | Sil.Hpointsto(_, Sil.Earray (len, _, _), _) ->
+          Some (len, prop)
       | _ -> None (* e points to something but not an array *)
     with Not_found -> (* e is not allocated, so we can add the array *)
-      let otyp' = (extract_array_type typ) in
-      match otyp' with
-      | Some 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), 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
-          let prop''= Prop.replace_sigma_footprint (hpred:: sigma_fp) prop' in
-          let prop''= Prop.normalize prop'' in
-          Some (size, prop'')
+    match extract_array_type typ with
+    | Some arr_typ ->
+        let len = Sil.Var (Ident.create_fresh Ident.kfootprint) in
+        let s = mk_empty_array_rearranged len in
+        let hpred = Prop.mk_ptsto n_lexp s (Sil.Sizeof (arr_typ, Some len, 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
+        let prop''= Prop.replace_sigma_footprint (hpred:: sigma_fp) prop' in
+        let prop''= Prop.normalize prop'' in
+        Some (len, prop'')
       | _ -> None
   end
 
@@ -97,31 +94,31 @@ let execute___require_allocated_array { Builtin.pdesc; prop_; path; ret_ids; arg
        | Some (_, prop) -> [(prop, path)])
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
-let execute___get_array_size { Builtin.pdesc; prop_; path; ret_ids; args; }
+let execute___get_array_length { Builtin.pdesc; prop_; path; ret_ids; args; }
   : Builtin.ret_typ =
   match args with
   | [(lexp, typ)] when IList.length ret_ids <= 1 ->
       (match add_array_to_prop pdesc prop_ lexp typ with
        | None -> []
-       | Some (size, prop) -> [(return_result size prop ret_ids, path)])
+       | Some (len, prop) -> [(return_result len prop ret_ids, path)])
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
-let execute___set_array_size { Builtin.pdesc; prop_; path; ret_ids; args; }
+let execute___set_array_length { Builtin.pdesc; prop_; path; ret_ids; args; }
   : Builtin.ret_typ =
   match args, ret_ids with
-  | [(lexp, typ); (size, _)], []->
+  | [(lexp, typ); (len, _)], []->
       (match add_array_to_prop pdesc prop_ lexp typ with
        | None -> []
        | Some (_, prop_a) -> (* Invariant: prop_a has an array pointed to by lexp *)
            let pname = Cfg.Procdesc.get_proc_name pdesc in
            let n_lexp, prop__ = check_arith_norm_exp pname lexp prop_a in
-           let n_size, prop = check_arith_norm_exp pname size prop__ in
+           let n_len, prop = check_arith_norm_exp pname len prop__ in
            let hpred, sigma' = IList.partition (function
                | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
                | _ -> false) (Prop.get_sigma prop) in
            (match hpred with
             | [Sil.Hpointsto(e, Sil.Earray(_, esel, inst), t)] ->
-                let hpred' = Sil.Hpointsto (e, Sil.Earray (n_size, esel, inst), t) in
+                let hpred' = Sil.Hpointsto (e, Sil.Earray (n_len, esel, inst), t) in
                 let prop' = Prop.replace_sigma (hpred':: sigma') prop in
                 [(Prop.normalize prop', path)]
             | _ -> [])) (* by construction of prop_a this case is impossible *)
@@ -162,8 +159,8 @@ let create_type tenv n_lexp typ prop =
             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 len = Sil.Var (Ident.create_fresh Ident.kfootprint) in
+            let sexp = mk_empty_array len in
             let texp = Sil.Sizeof (typ, None, Sil.Subtype.subtypes) in
             let hpred = Prop.mk_ptsto n_lexp sexp texp in
             Some hpred
@@ -763,11 +760,9 @@ let execute_alloc mk can_return_null
     | Sil.Const _ | Sil.Cast _ | Sil.Lvar _ | Sil.Lfield _ | Sil.Lindex _ -> e
     | 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 (Sil.Tarray (Sil.Tint ik, Some len), None, _) when Sil.ikind_is_char ik ->
+        evaluate_char_sizeof (Sil.Const (Sil.Cint len))
     | Sil.Sizeof _ -> e 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
@@ -790,7 +785,8 @@ let execute_alloc mk can_return_null
     let n_size_exp, prop = check_arith_norm_exp pname size_exp prop_ in
     let n_size_exp' = evaluate_char_sizeof n_size_exp in
     Prop.exp_normalize_prop prop n_size_exp', prop in
-  let cnt_te = handle_sizeof_exp size_exp' in
+  let cnt_te =
+    Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, None), Some size_exp', Sil.Subtype.exact) in
   let id_new = Ident.create_fresh Ident.kprimed in
   let exp_new = Sil.Var id_new in
   let ptsto_new =
@@ -989,9 +985,9 @@ let __delete_array = Builtin.register
 let __exit = Builtin.register
     (* _exit from C library *)
     "_exit" execute_exit
-let __get_array_size = Builtin.register
-    (* return the size of the array passed as a parameter *)
-    "__get_array_size" execute___get_array_size
+let __get_array_length = Builtin.register
+    (* return the length of the array passed as a parameter *)
+    "__get_array_length" execute___get_array_length
 let __require_allocated_array = Builtin.register
     (* require the parameter to point to an allocated array *)
     "__require_allocated_array" execute___require_allocated_array
@@ -1053,9 +1049,9 @@ let __placement_new = Builtin.register
 let _ = Builtin.register
     (* print a value as seen by the engine *)
     "__print_value" execute___print_value
-let __set_array_size = Builtin.register
-    (* set the size of the array passed as a parameter *)
-    "__set_array_size" execute___set_array_size
+let __set_array_length = Builtin.register
+    (* set the length of the array passed as a parameter *)
+    "__set_array_length" execute___set_array_length
 let __set_autorelease_attribute = Builtin.register
     (* set the attribute of the parameter as autorelease *)
     "__set_autorelease_attribute" execute___set_autorelease_attribute
diff --git a/infer/src/backend/modelBuiltins.mli b/infer/src/backend/modelBuiltins.mli
index 991d638d1..e4109e0d6 100644
--- a/infer/src/backend/modelBuiltins.mli
+++ b/infer/src/backend/modelBuiltins.mli
@@ -15,7 +15,7 @@ val __assert_fail : Procname.t
 val __delete : Procname.t
 val __delete_array : Procname.t
 val __exit : Procname.t
-val __get_array_size : Procname.t
+val __get_array_length : Procname.t
 val __get_type_of : Procname.t
 val __infer_fail : Procname.t
 val __instanceof : Procname.t (** [__instanceof(val,typ)] implements java's [val instanceof typ] *)
@@ -26,7 +26,7 @@ val __new : Procname.t
 val __new_array : Procname.t
 val __objc_alloc : Procname.t
 val __objc_alloc_no_fail : Procname.t
-val __set_array_size : Procname.t
+val __set_array_length : Procname.t
 val __unwrap_exception : Procname.t
 val __set_file_attribute : Procname.t
 val __set_mem_attribute : Procname.t
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index 21e352862..e2893645e 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -456,10 +456,12 @@ let sym_eval abs e =
         Sil.Const (Sil.Cclosure { c with captured_vars; })
     | Sil.Const _ ->
         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 ->
+      when Sil.ikind_is_char ik && !Config.curr_language = Config.Clang ->
         eval l
+    | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, Some l), _, _)
+      when Sil.ikind_is_char ik && !Config.curr_language = Config.Clang ->
+        Sil.Const (Sil.Cint l)
     | Sil.Sizeof _ ->
         e
     | Sil.Cast (_, e1) ->
@@ -592,53 +594,31 @@ let sym_eval abs e =
         (* progress: convert inner +I to +A *)
         let e2' = Sil.BinOp (Sil.PlusA, e12, e2) in
         eval (Sil.BinOp (Sil.PlusPI, e11, e2'))
-    | Sil.BinOp
-        (Sil.PlusA,
-         (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
-           struct s { ... t arr[n + k] ... } *)
-        let e1' = eval e1 in
-        let e2' = eval e2 in
-        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, 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', None, st)
-         | _ -> Sil.BinOp(Sil.PlusA, e1', e2'))
     | Sil.BinOp (Sil.PlusA as oplus, e1, e2)
     | Sil.BinOp (Sil.PlusPI as oplus, e1, e2) ->
         let e1' = eval e1 in
         let e2' = eval e2 in
         let isPlusA = oplus = Sil.PlusA in
         let ominus = if isPlusA then Sil.MinusA else Sil.MinusPI in
-        let (+++) x y = match y with
-          | Sil.Const (Sil.Cint i) when Sil.Int.iszero i -> x
+        let (+++) x y = match x, y with
+          | _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i -> x
+          | Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (Sil.Int.add i j))
           | _ -> Sil.BinOp (oplus, x, y) in
-        let (---) x y = match y with
-          | Sil.Const (Sil.Cint i) when Sil.Int.iszero i -> x
+        let (---) x y = match x, y with
+          | _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i -> x
+          | Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (Sil.Int.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 =
+          Option.map_default (Sil.typ_equal elt) false (Sil.get_extensible_array_element_typ typ) 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)
+          (* pattern for arrays and extensible structs:
+             sizeof(struct s {... t[l]}) + k * sizeof(t)) = sizeof(struct s {... t[l + k]}) *)
+          | Sil.Sizeof (typ, len1_opt, st), Sil.BinOp (Sil.Mult, len2, Sil.Sizeof (elt, None, _))
+            when isPlusA && (extensible_array_element_typ_equal elt typ) ->
+              let len = match len1_opt with Some len1 -> len1 +++ len2 | None -> len2 in
+              Sil.Sizeof (typ, Some len, st)
           | Sil.Const c, _ when iszero_int_float c ->
               e2'
           | _, Sil.Const c when iszero_int_float c ->
@@ -750,10 +730,13 @@ let sym_eval abs e =
           | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
               Sil.exp_float (v /.w)
           | 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
+          | Sil.Sizeof (Sil.Tarray (elt, Some len), None, _), Sil.Sizeof (elt2, None, _)
+            (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
+            when Sil.typ_equal elt elt2 ->
+              Sil.Const (Sil.Cint len)
           | _ ->
               if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.Div, e1', e2')
         end
@@ -852,65 +835,10 @@ let exp_normalize sub exp =
   if !Config.abs_val >= 1 then sym_eval true exp'
   else sym_eval false exp'
 
-let rec texp_normalize sub exp = match exp with
-  | Sil.Sizeof (typ, len, st) ->
-      Sil.Sizeof (typ_normalize sub typ, Option.map (exp_normalize sub) len, st)
+let texp_normalize sub exp = match exp with
+  | Sil.Sizeof (typ, len, st) -> Sil.Sizeof (typ, Option.map (exp_normalize sub) len, st)
   | _ -> exp_normalize sub exp
 
-(* NOTE: usage of == operator in flds_norm and typ_normalize is intended*)
-(* to decrease pressure on ocaml's GC and not allocate new objects if typ_normalize*)
-(* doesn't change anything in structure of the type *)
-and flds_norm sub fields =
-  let fld_norm ((f, t, a) as field) =
-    let t' = typ_normalize sub t in
-    if t' == t then
-      field
-    else
-      (f, t', a) in
-
-  let rec flds_norm_aux fields = match fields with
-    | [] -> fields
-    | field :: rest ->
-        let rest' = flds_norm_aux rest in
-        let field' = fld_norm field in
-        if field == field' && rest == rest' then
-          fields
-        else
-          field' :: rest' in
-  flds_norm_aux fields
-
-and typ_normalize sub typ = match typ with
-  | Sil.Tvar _
-  | Sil.Tint _
-  | Sil.Tfloat _
-  | Sil.Tvoid
-  | Sil.Tfun _ ->
-      typ
-  | Sil.Tptr (t, pk) ->
-      let t' = typ_normalize sub t in
-      if t == t' then
-        typ
-      else
-        Sil.Tptr (t', pk)
-  | Sil.Tstruct struct_typ ->
-      let instance_fields = struct_typ.Sil.instance_fields in
-      let instance_fields' = flds_norm sub instance_fields in
-      let static_fields = struct_typ.Sil.static_fields in
-      let static_fields' = flds_norm sub static_fields in
-      if instance_fields == instance_fields' && static_fields == static_fields' then
-        typ
-      else
-        Sil.Tstruct
-          { struct_typ with
-            Sil.instance_fields = instance_fields';
-            static_fields = static_fields';
-        }
-  | Sil.Tarray (t, e) ->
-      (* this case is not optimized for less GC allocations since it requires*)
-      (* to make exp_normalize GC-friendly as well. Profiling showed that it's fine*)
-      (* to keep this code not optimized *)
-      Sil.Tarray (typ_normalize sub t, exp_normalize sub e)
-
 let run_with_abs_val_eq_zero f =
   let abs_val_old = !Config.abs_val in
   Config.abs_val := 0;
@@ -1136,12 +1064,12 @@ let rec strexp_normalize sub se =
             let fld_cnts'' = IList.sort Sil.fld_strexp_compare fld_cnts' in
             Sil.Estruct (fld_cnts'', inst)
       end
-  | Sil.Earray (size, idx_cnts, inst) ->
+  | Sil.Earray (len, idx_cnts, inst) ->
       begin
-        let size' = exp_normalize_noabs sub size in
+        let len' = exp_normalize_noabs sub len in
         match idx_cnts with
         | [] ->
-            if Sil.exp_equal size size' then se else Sil.Earray (size', idx_cnts, inst)
+            if Sil.exp_equal len len' then se else Sil.Earray (len', idx_cnts, inst)
         | _ ->
             let idx_cnts' =
               IList.map (fun (idx, cnt) ->
@@ -1149,7 +1077,7 @@ let rec strexp_normalize sub se =
                   idx', strexp_normalize sub cnt) idx_cnts in
             let idx_cnts'' =
               IList.sort Sil.exp_strexp_compare idx_cnts' in
-            Sil.Earray (size', idx_cnts'', inst)
+            Sil.Earray (len', idx_cnts'', inst)
       end
 
 (** create a strexp of the given type, populating the structures if [expand_structs] is true *)
@@ -1184,8 +1112,11 @@ let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
           let flds, _ = IList.fold_right f instance_fields ([], len) in
           Sil.Estruct (flds, inst)
     )
-  | Sil.Tarray (_, size), None ->
-      Sil.Earray (size, [], inst)
+  | Sil.Tarray (_, len_opt), None ->
+      let len = match len_opt with
+        | None -> Sil.exp_get_undefined false
+        | Some len -> Sil.Const (Sil.Cint len) in
+      Sil.Earray (len, [], inst)
   | Sil.Tarray _, Some len ->
       Sil.Earray (len, [], inst)
   | Sil.Tvar _, _
@@ -1216,8 +1147,8 @@ let mk_ptsto_exp tenvo struct_init_mode (exp, te, expo) inst : Sil.hpred =
   mk_ptsto exp strexp te
 
 let replace_array_contents hpred esel = match hpred with
-  | Sil.Hpointsto (root, Sil.Earray (size, [], inst), te) ->
-      Sil.Hpointsto (root, Sil.Earray (size, esel, inst), te)
+  | Sil.Hpointsto (root, Sil.Earray (len, [], inst), te) ->
+      Sil.Hpointsto (root, Sil.Earray (len, esel, inst), te)
   | _ -> assert false
 
 let rec hpred_normalize sub hpred =
@@ -2345,39 +2276,20 @@ 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, len, st) ->
-      Sil.Sizeof (typ_captured_ren ren t, Option.map (exp_captured_ren ren) len, st)
+  | Sil.Sizeof (t, len, st) -> Sil.Sizeof (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
-        | Some t -> Some (typ_captured_ren ren t)
-        | None -> None in
-      Sil.UnOp (op, exp_captured_ren ren e, topt')
+  | Sil.UnOp (op, e, topt) -> Sil.UnOp (op, exp_captured_ren ren e, topt)
   | Sil.BinOp (op, e1, e2) ->
       let e1' = exp_captured_ren ren e1 in
       let e2' = exp_captured_ren ren e2 in
       Sil.BinOp (op, e1', e2')
   | Sil.Lvar id -> Sil.Lvar id
-  | Sil.Lfield (e, fld, typ) -> Sil.Lfield (exp_captured_ren ren e, fld, typ_captured_ren ren typ)
+  | Sil.Lfield (e, fld, typ) -> Sil.Lfield (exp_captured_ren ren e, fld, typ)
   | Sil.Lindex (e1, e2) ->
       let e1' = exp_captured_ren ren e1 in
       let e2' = exp_captured_ren ren e2 in
       Sil.Lindex(e1', e2')
 
-(* Apply a renaming function to a type *)
-and typ_captured_ren ren typ = match typ with
-  | Sil.Tvar _
-  | Sil.Tint _
-  | Sil.Tfloat _
-  | Sil.Tvoid
-  | Sil.Tstruct _
-  | Sil.Tfun _ ->
-      typ
-  | Sil.Tptr (t', pk) ->
-      Sil.Tptr (typ_captured_ren ren t', pk)
-  | Sil.Tarray (t, e) ->
-      Sil.Tarray (typ_captured_ren ren t, exp_captured_ren ren e)
-
 let atom_captured_ren ren = function
   | Sil.Aeq (e1, e2) ->
       Sil.Aeq (exp_captured_ren ren e1, exp_captured_ren ren e2)
@@ -2390,12 +2302,12 @@ let rec strexp_captured_ren ren = function
   | Sil.Estruct (fld_se_list, inst) ->
       let f (fld, se) = (fld, strexp_captured_ren ren se) in
       Sil.Estruct (IList.map f fld_se_list, inst)
-  | Sil.Earray (size, idx_se_list, inst) ->
+  | Sil.Earray (len, idx_se_list, inst) ->
       let f (idx, se) =
         let idx' = exp_captured_ren ren idx in
         (idx', strexp_captured_ren ren se) in
-      let size' = exp_captured_ren ren size in
-      Sil.Earray (size', IList.map f idx_se_list, inst)
+      let len' = exp_captured_ren ren len in
+      Sil.Earray (len', IList.map f idx_se_list, inst)
 
 and hpred_captured_ren ren = function
   | Sil.Hpointsto (base, se, te) ->
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index 50477a07d..a2ec12868 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -380,8 +380,8 @@ end = struct
       | Sil.Eexp _ -> ()
       | Sil.Estruct (fsel, _) ->
           IList.iter (fun (_, se) -> strexp_extract se) fsel
-      | Sil.Earray (size, isel, _) ->
-          add_lt_minus1_e size;
+      | Sil.Earray (len, isel, _) ->
+          add_lt_minus1_e len;
           IList.iter (fun (idx, se) ->
               add_lt_minus1_e idx;
               strexp_extract se) isel in
@@ -909,7 +909,7 @@ module ProverState : sig
   val checks : check list ref
 
   type bounds_check = (** type for array bounds checks *)
-    | BCsize_imply of Sil.exp * Sil.exp * Sil.exp list (** coming from array_size_imply *)
+    | BClen_imply of Sil.exp * Sil.exp * Sil.exp list (** coming from array_len_imply *)
     | BCfrom_pre of Sil.atom (** coming implicitly from preconditions *)
 
   val add_bounds_check : bounds_check -> unit
@@ -934,12 +934,12 @@ module ProverState : sig
   val d_implication_error : string * (Sil.subst * Sil.subst) * exc_body -> unit
 end = struct
   type bounds_check =
-    | BCsize_imply of Sil.exp * Sil.exp * Sil.exp list
+    | BClen_imply of Sil.exp * Sil.exp * Sil.exp list
     | BCfrom_pre of Sil.atom
 
   let implication_lhs = ref Prop.prop_emp
   let implication_rhs = ref (Prop.expose Prop.prop_emp)
-  let fav_in_array_size = ref (Sil.fav_new ()) (* free variables in array size position *)
+  let fav_in_array_len = ref (Sil.fav_new ()) (* free variables in array len position *)
   let bounds_checks = ref [] (* delayed bounds check for arrays *)
   let frame_fld = ref []
   let missing_fld = ref []
@@ -949,12 +949,12 @@ end = struct
   let missing_typ = ref []
   let checks = ref []
 
-  (** free vars in array size position in current part of prop *)
-  let prop_fav_size prop =
+  (** free vars in array len position in current strexp part of prop *)
+  let prop_fav_len prop =
     let fav = Sil.fav_new () in
     let do_hpred = function
-      | Sil.Hpointsto (_, Sil.Earray (Sil.Var _ as size, _, _), _) ->
-          Sil.exp_fav_add fav size
+      | Sil.Hpointsto (_, Sil.Earray (Sil.Var _ as len, _, _), _) ->
+          Sil.exp_fav_add fav len
       | _ -> () in
     IList.iter do_hpred (Prop.get_sigma prop);
     fav
@@ -963,7 +963,7 @@ end = struct
     checks := [];
     implication_lhs := lhs;
     implication_rhs := rhs;
-    fav_in_array_size := prop_fav_size rhs;
+    fav_in_array_len := prop_fav_len rhs;
     bounds_checks := [];
     frame_fld := [];
     frame_typ := [];
@@ -993,11 +993,12 @@ end = struct
   let add_missing_sigma sigma =
     missing_sigma := sigma @ !missing_sigma
 
-  (** atom considered array bounds check if it contains vars present in array size position in the pre *)
+  (** atom considered array bounds check if it contains vars present in array length position in the
+      pre *)
   let atom_is_array_bounds_check atom =
     let fav_a = Sil.atom_fav atom in
     Prop.atom_is_inequality atom &&
-    Sil.fav_exists fav_a (fun a -> Sil.fav_mem !fav_in_array_size a)
+    Sil.fav_exists fav_a (fun a -> Sil.fav_mem !fav_in_array_len a)
 
   let get_bounds_checks () = !bounds_checks
   let get_frame_fld () = !frame_fld
@@ -1213,18 +1214,18 @@ let path_to_id path =
     | None -> Ident.create_fresh Ident.kfootprint
     | Some s -> Ident.create_path s
 
-(** Implication for the size of arrays *)
-let array_size_imply calc_missing subs size1 size2 indices2 =
-  match size1, size2 with
+(** Implication for the length of arrays *)
+let array_len_imply calc_missing subs len1 len2 indices2 =
+  match len1, len2 with
   | _, Sil.Var _
   | _, Sil.BinOp (Sil.PlusA, Sil.Var _, _)
   | _, Sil.BinOp (Sil.PlusA, _, Sil.Var _)
   | Sil.BinOp (Sil.Mult, _, _), _ ->
-      (try exp_imply calc_missing subs size1 size2 with
+      (try exp_imply calc_missing subs len1 len2 with
        | IMPL_EXC (s, subs', x) ->
-           raise (IMPL_EXC ("array size:" ^ s, subs', x)))
+           raise (IMPL_EXC ("array len:" ^ s, subs', x)))
   | _ ->
-      ProverState.add_bounds_check (ProverState.BCsize_imply (size1, size2, indices2));
+      ProverState.add_bounds_check (ProverState.BClen_imply (len1, len2, indices2));
       subs
 
 (** Extend [sub1] and [sub2] to witnesses that each instance of
@@ -1252,18 +1253,18 @@ let rec sexp_imply source calc_index_frame calc_missing subs se1 se2 typ2 : subs
             d_impl_err ("sexp_imply not implemented", subs, (EXC_FALSE_SEXPS (se1, se2)));
             raise (Exceptions.Abduction_case_not_implemented __POS__)
       end
-  | Sil.Earray (size1, esel1, inst1), Sil.Earray (size2, esel2, _) ->
+  | Sil.Earray (len1, esel1, inst1), Sil.Earray (len2, esel2, _) ->
       let indices2 = IList.map fst esel2 in
-      let subs' = array_size_imply calc_missing subs size1 size2 indices2 in
+      let subs' = array_len_imply calc_missing subs len1 len2 indices2 in
       let subs'', index_frame, index_missing =
         array_imply source calc_index_frame calc_missing subs' esel1 esel2 typ2 in
       let index_frame_opt = if index_frame != []
-        then Some (Sil.Earray (size1, index_frame, inst1))
+        then Some (Sil.Earray (len1, index_frame, inst1))
         else None in
       let index_missing_opt =
         if index_missing != [] &&
            (Config.allow_missing_index_in_proc_call || !Config.footprint)
-        then Some (Sil.Earray (size1, index_missing, inst1))
+        then Some (Sil.Earray (len1, index_missing, inst1))
         else None in
       subs'', index_frame_opt, index_missing_opt
   | Sil.Eexp (_, inst), Sil.Estruct (fsel, inst') ->
@@ -1272,13 +1273,17 @@ let rec sexp_imply source calc_index_frame calc_missing subs se1 se2 typ2 : subs
         let g (f, _) = (f, Sil.Eexp (Sil.Var (Ident.create_fresh Ident.knormal), inst)) in
         IList.map g fsel in
       sexp_imply source calc_index_frame calc_missing subs (Sil.Estruct (fsel', inst')) se2 typ2
-  | Sil.Eexp _, Sil.Earray (size, _, inst)
-  | Sil.Estruct _, Sil.Earray (size, _, inst) ->
-      let se1' = Sil.Earray (size, [(Sil.exp_zero, se1)], inst) in
+  | Sil.Eexp _, Sil.Earray (len, _, inst)
+  | Sil.Estruct _, Sil.Earray (len, _, inst) ->
+      let se1' = Sil.Earray (len, [(Sil.exp_zero, se1)], inst) in
       sexp_imply source calc_index_frame calc_missing subs se1' se2 typ2
-  | Sil.Earray (size, _, _), Sil.Eexp (_, inst) ->
-      let se2' = Sil.Earray (size, [(Sil.exp_zero, se2)], inst) in
-      let typ2' = Sil.Tarray (typ2, size) in
+  | Sil.Earray (len, _, _), Sil.Eexp (_, inst) ->
+      let se2' = Sil.Earray (len, [(Sil.exp_zero, se2)], inst) in
+      let typ2' = Sil.Tarray (typ2, None) in
+      (* In the sexp_imply, struct_imply, array_imply, and sexp_imply_nolhs functions, the typ2
+         argument is only used by eventually passing its value to Sil.struct_typ_fld, Sil.Lfield,
+         Sil.struct_typ_fld, or Sil.array_typ_elem.  None of these are sensitive to the length field
+         of Tarray, so forgetting the length of typ2' here is not a problem. *)
       sexp_imply source true calc_missing subs se1 se2' typ2' (* calculate index_frame because the rhs is a singleton array *)
   | _ ->
       d_impl_err ("sexp_imply not implemented", subs, (EXC_FALSE_SEXPS (se1, se2)));
@@ -1442,18 +1447,19 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred =
         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 clen = Sil.exp_get_undefined false in
         let t' = match t with
-          | Sil.Sizeof (t_, vlen, st) ->
-              Sil.Sizeof (Sil.Tarray (t_, clen), vlen, st)
+          | Sil.Sizeof (t_, len, st) -> Sil.Sizeof (Sil.Tarray (t_, None), len, st)
           | _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in
-        let hpred' = Sil.Hpointsto (e, Sil.Earray (clen, [(ind, se)], Sil.inst_none), t') in
+        let len = match t' with
+          | Sil.Sizeof (_, Some len, _) -> len
+          | _ -> Sil.exp_get_undefined false in
+        let hpred' = Sil.Hpointsto (e, Sil.Earray (len, [(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) ->
+    | Sil.Hpointsto (Sil.BinOp (Sil.PlusPI, e1, e2), Sil.Earray (len, esel, inst), t) ->
         let shift_exp e = Sil.BinOp (Sil.PlusA, e, e2) in
-        let size' = shift_exp size in
+        let len' = shift_exp len in
         let esel' = IList.map (fun (e, se) -> (shift_exp e, se)) esel in
-        let hpred' = Sil.Hpointsto (e1, Sil.Earray (size', esel', inst), t) in
+        let hpred' = Sil.Hpointsto (e1, Sil.Earray (len', esel', inst), t) in
         expand true calc_index_frame hpred'
     | _ -> changed, calc_index_frame, hpred in
   expand false calc_index_frame hpred
@@ -1687,8 +1693,8 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
   else
     None, None
 
-(** pre-process implication between a non-array and an array: the non-array is turned into an array of size given by its type
-    only active in type_size mode *)
+(** pre-process implication between a non-array and an array: the non-array is turned into an array
+    of length given by its type only active in type_size mode *)
 let sexp_imply_preprocess se1 texp1 se2 = match se1, texp1, se2 with
   | Sil.Eexp (_, inst), Sil.Sizeof _, Sil.Earray _ when Config.type_size ->
       let se1' = Sil.Earray (texp1, [(Sil.exp_zero, se1)], inst) in
@@ -1941,13 +1947,14 @@ 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 len = Sil.exp_int (Sil.Int.of_int (1 + String.length s)) in
+    let len = 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 (len, [(index, Sil.Eexp (Sil.exp_zero, Sil.inst_none))], Sil.inst_none)
+          Sil.Earray
+            (Sil.exp_int 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
@@ -1958,7 +1965,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
     let const_string_texp =
       match !Config.curr_language with
       | Config.Clang ->
-          Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, len), Some len, Sil.Subtype.exact)
+          Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, Some len), None, Sil.Subtype.exact)
       | Config.Java ->
           let object_type =
             Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.String") in
@@ -2107,13 +2114,14 @@ let check_array_bounds (sub1, sub2) prop =
     let lt_ineq = Prop.mk_inequality (Sil.BinOp(Sil.Le, e', e'')) in
     if check_atom prop lt_ineq then check_failed lt_ineq in
   let check_bound = function
-    | ProverState.BCsize_imply (_size1, _size2, _indices2) ->
-        let size1 = Sil.exp_sub sub1 _size1 in
-        let size2 = Sil.exp_sub sub2 _size2 in
-        (* L.d_strln_color Orange "check_bound "; Sil.d_exp size1; L.d_str " "; Sil.d_exp size2; L.d_ln(); *)
-        let indices_to_check = match size2 with
-          | _ -> [Sil.BinOp(Sil.PlusA, size2, Sil.exp_minus_one)] (* only check size *) in
-        IList.iter (fail_if_le size1) indices_to_check
+    | ProverState.BClen_imply (len1_, len2_, _indices2) ->
+        let len1 = Sil.exp_sub sub1 len1_ in
+        let len2 = Sil.exp_sub sub2 len2_ in
+        (* L.d_strln_color Orange "check_bound ";
+           Sil.d_exp len1; L.d_str " "; Sil.d_exp len2; L.d_ln(); *)
+        let indices_to_check = match len2 with
+          | _ -> [Sil.BinOp(Sil.PlusA, len2, Sil.exp_minus_one)] (* only check len *) in
+        IList.iter (fail_if_le len1) indices_to_check
     | ProverState.BCfrom_pre _atom ->
         let atom_neg = Prop.atom_negate (Sil.atom_sub sub2 _atom) in
         (* L.d_strln_color Orange "BCFrom_pre"; Sil.d_atom atom_neg; L.d_ln (); *)
@@ -2152,8 +2160,10 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
     let sigma1' = Prop.sigma_sub sub1 sigma1 in
     L.d_ln ();
     let prop_for_impl = prepare_prop_for_implication (sub1, sub2) pi1' sigma1' in
-    imply_pi calc_missing (sub1, sub2) prop_for_impl pi2_nobcheck; (* only deal with pi2 without bound checks *)
-    check_array_bounds (sub1, sub2) prop_for_impl; (* handle implicit bound checks, plus those from array_size_imply *)
+    (* only deal with pi2 without bound checks *)
+    imply_pi calc_missing (sub1, sub2) prop_for_impl pi2_nobcheck;
+    (* handle implicit bound checks, plus those from array_len_imply *)
+    check_array_bounds (sub1, sub2) prop_for_impl;
     L.d_strln "Result of Abduction";
     L.d_increase_indent 1; d_impl (sub1, sub2) (prop1, prop2); L.d_decrease_indent 1; L.d_ln ();
     L.d_strln"returning TRUE";
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index 015162294..d518e6500 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -28,23 +28,23 @@ let rec list_rev_and_concat l1 l2 =
   | x1:: l1' -> list_rev_and_concat l1' (x1:: l2)
 
 (** Check whether the index is out of bounds.
-    If the size is - 1, no check is performed.
+    If the length is - 1, no check is performed.
     If the index is provably out of bound, a bound error is given.
-    If the size is a constant and the index is not provably in bound, a warning is given.
+    If the length is a constant and the index is not provably in bound, a warning is given.
 *)
-let check_bad_index pname p size index loc =
-  let size_is_constant = match size with
+let check_bad_index pname p len index loc =
+  let len_is_constant = match len with
     | Sil.Const _ -> true
     | _ -> false in
   let index_provably_out_of_bound () =
-    let index_too_large = Prop.mk_inequality (Sil.BinOp(Sil.Le, size, index)) in
-    let index_negative = Prop.mk_inequality (Sil.BinOp(Sil.Le, index, Sil.exp_minus_one)) in
+    let index_too_large = Prop.mk_inequality (Sil.BinOp (Sil.Le, len, index)) in
+    let index_negative = Prop.mk_inequality (Sil.BinOp (Sil.Le, index, Sil.exp_minus_one)) in
     (Prover.check_atom p index_too_large) || (Prover.check_atom p index_negative) in
   let index_provably_in_bound () =
-    let size_minus_one = Sil.BinOp(Sil.PlusA, size, Sil.exp_minus_one) in
-    let index_not_too_large = Prop.mk_inequality (Sil.BinOp(Sil.Le, index, size_minus_one)) in
+    let len_minus_one = Sil.BinOp(Sil.PlusA, len, Sil.exp_minus_one) in
+    let index_not_too_large = Prop.mk_inequality (Sil.BinOp(Sil.Le, index, len_minus_one)) in
     let index_nonnegative = Prop.mk_inequality (Sil.BinOp(Sil.Le, Sil.exp_zero, index)) in
-    Prover.check_zero index || (* index 0 always in bound, even when we know nothing about size *)
+    Prover.check_zero index || (* index 0 always in bound, even when we know nothing about len *)
     ((Prover.check_atom p index_not_too_large) && (Prover.check_atom p index_nonnegative)) in
   let index_has_bounds () =
     match Prover.get_bounds p index with
@@ -55,17 +55,17 @@ let check_bad_index pname p size index loc =
     | _ -> None in
   if not (index_provably_in_bound ()) then
     begin
-      let size_const_opt = get_const_opt size in
+      let len_const_opt = get_const_opt len in
       let index_const_opt = get_const_opt index in
       if index_provably_out_of_bound () then
-        let deref_str = Localise.deref_str_array_bound size_const_opt index_const_opt in
+        let deref_str = Localise.deref_str_array_bound len_const_opt index_const_opt in
         let exn =
           Exceptions.Array_out_of_bounds_l1
             (Errdesc.explain_array_access deref_str p loc, __POS__) in
         let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
         Reporting.log_warning pname ~pre: pre_opt exn
-      else if size_is_constant then
-        let deref_str = Localise.deref_str_array_bound size_const_opt index_const_opt in
+      else if len_is_constant then
+        let deref_str = Localise.deref_str_array_bound len_const_opt index_const_opt in
         let desc = Errdesc.explain_array_access deref_str p loc in
         let exn = if index_has_bounds ()
           then Exceptions.Array_out_of_bounds_l2 (desc, __POS__)
@@ -75,14 +75,14 @@ let check_bad_index pname p size index loc =
     end
 
 (** Perform bounds checking *)
-let bounds_check pname prop size e =
+let bounds_check pname prop len e =
   if Config.trace_rearrange then
     begin
       L.d_str "Bounds check index:"; Sil.d_exp e;
-      L.d_str " size: "; Sil.d_exp size;
+      L.d_str " len: "; Sil.d_exp len;
       L.d_ln()
     end;
-  check_bad_index pname prop size e
+  check_bad_index pname prop len e
 
 let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp t
     (off: Sil.offset list) inst : Sil.atom list * Sil.strexp * Sil.typ =
@@ -112,7 +112,8 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
           create_struct_values
             pname tenv orig_prop footprint_part kind max_stamp t' off' inst in
         let se = Sil.Estruct ([(f, se')], inst) in
-        let replace_typ_of_f (f', t', a') = if Ident.fieldname_equal f f' then (f, res_t', a') else (f', t', a') in
+        let replace_typ_of_f (f', t', a') =
+          if Ident.fieldname_equal f f' then (f, res_t', a') else (f', t', a') in
         let instance_fields' =
           IList.sort Sil.fld_typ_ann_compare (IList.map replace_typ_of_f instance_fields) in
         (atoms', se, Sil.Tstruct { struct_typ with Sil.instance_fields = instance_fields'})
@@ -121,25 +122,29 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
           create_struct_values
             pname tenv orig_prop footprint_part kind max_stamp t off' inst in
         let e' = Sil.array_clean_new_index footprint_part e in
-        let size = Sil.exp_get_undefined false in
-        let se = Sil.Earray (size, [(e', se')], inst) in
-        let res_t = Sil.Tarray (res_t', size) in
-        (Sil.Aeq(e, e'):: atoms', se, res_t)
-    | Sil.Tarray(_, size),[] ->
-        ([], Sil.Earray(size, [], inst), t)
-    | Sil.Tarray(t', size'), (Sil.Off_index e) :: off' ->
-        bounds_check pname orig_prop size' e (State.get_loc ());
-
-        let atoms', se', res_t' =
-          create_struct_values
-            pname tenv orig_prop footprint_part kind max_stamp t' off' inst in
-        let e' = Sil.array_clean_new_index footprint_part e in
-        let se = Sil.Earray(size', [(e', se')], inst) in
-        let res_t = Sil.Tarray(res_t', size') in
-        (Sil.Aeq(e, e'):: atoms', se, res_t)
-    | Sil.Tarray _, (Sil.Off_fld _) :: _ ->
-        assert false
-
+        let len = Sil.Var (new_id ()) in
+        let se = Sil.Earray (len, [(e', se')], inst) in
+        let res_t = Sil.Tarray (res_t', None) in
+        (Sil.Aeq(e, e') :: atoms', se, res_t)
+    | Sil.Tarray (t', len_), off ->
+        let len = match len_ with
+          | None -> Sil.Var (new_id ())
+          | Some len -> Sil.Const (Sil.Cint len) in
+        (match off with
+         | [] ->
+             ([], Sil.Earray (len, [], inst), t)
+         | (Sil.Off_index e) :: off' ->
+             bounds_check pname orig_prop len e (State.get_loc ());
+             let atoms', se', res_t' =
+               create_struct_values
+                 pname tenv orig_prop footprint_part kind max_stamp t' off' inst in
+             let e' = Sil.array_clean_new_index footprint_part e in
+             let se = Sil.Earray (len, [(e', se')], inst) in
+             let res_t = Sil.Tarray (res_t', len_) in
+             (Sil.Aeq(e, e') :: atoms', se, res_t)
+         | (Sil.Off_fld _) :: _ ->
+             assert false
+        )
     | Sil.Tint _, [] | Sil.Tfloat _, [] | Sil.Tvoid, [] | Sil.Tfun _, [] | Sil.Tptr _, [] ->
         let id = new_id () in
         ([], Sil.Eexp (Sil.Var id, inst), t)
@@ -150,14 +155,13 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
         let t' = match t with
           | Sil.Tptr(t', _) -> t'
           | _ -> t in
-        let size = Sil.Var (new_id ()) in
-
+        let len = Sil.Var (new_id ()) in
         let atoms', se', res_t' =
           create_struct_values
             pname tenv orig_prop footprint_part kind max_stamp t' [] inst in
         let e' = Sil.array_clean_new_index footprint_part e in
-        let se = Sil.Earray(size, [(e', se')], inst) in
-        let res_t = Sil.Tarray(res_t', size) in
+        let se = Sil.Earray (len, [(e', se')], inst) in
+        let res_t = Sil.Tarray (res_t', None) in
         (Sil.Aeq(e, e'):: atoms', se, res_t)
     | Sil.Tint _, _ | Sil.Tfloat _, _ | Sil.Tvoid, _ | Sil.Tfun _, _ | Sil.Tptr _, _ ->
         L.d_str "create_struct_values type:"; Sil.d_typ_full t; L.d_str " off: "; Sil.d_offset_list off; L.d_ln();
@@ -185,6 +189,9 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
 let rec _strexp_extend_values
     pname tenv orig_prop footprint_part kind max_stamp
     se typ (off : Sil.offset list) inst =
+  let new_id () =
+    incr max_stamp;
+    Ident.create kind !max_stamp in
   match off, se, typ with
   | [], Sil.Eexp _, _
   | [], Sil.Estruct _, _ ->
@@ -193,7 +200,7 @@ let rec _strexp_extend_values
       let off_new = Sil.Off_index(Sil.exp_zero):: off in
       _strexp_extend_values
         pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
-  | (Sil.Off_fld _):: _, Sil.Earray _, Sil.Tarray _ ->
+  | (Sil.Off_fld _) :: _, Sil.Earray _, Sil.Tarray _ ->
       let off_new = Sil.Off_index(Sil.exp_zero):: off in
       _strexp_extend_values
         pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
@@ -243,18 +250,17 @@ let rec _strexp_extend_values
   | (Sil.Off_index _):: _, Sil.Eexp _, Sil.Tptr _
   | (Sil.Off_index _):: _, Sil.Estruct _, Sil.Tstruct _ ->
       (* L.d_strln_color Orange "turn into an array"; *)
-      let size = match se with
-        | Sil.Eexp (_, Sil.Ialloc) -> Sil.exp_one (* if allocated explicitly, we know size is 1 *)
+      let len = match se with
+        | Sil.Eexp (_, Sil.Ialloc) -> Sil.exp_one (* if allocated explicitly, we know len is 1 *)
         | _ ->
             if Config.type_size then Sil.exp_one (* Sil.Sizeof (typ, Sil.Subtype.exact) *)
-            else Sil.exp_get_undefined false in
-
-      let se_new = Sil.Earray(size, [(Sil.exp_zero, se)], inst) in
-      let typ_new = Sil.Tarray(typ, size) in
+            else Sil.Var (new_id ()) in
+      let se_new = Sil.Earray (len, [(Sil.exp_zero, se)], inst) in
+      let typ_new = Sil.Tarray (typ, None) in
       _strexp_extend_values
         pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off inst
-  | (Sil.Off_index e):: off', Sil.Earray(size, esel, inst_arr), Sil.Tarray(typ', size_for_typ') ->
-      bounds_check pname orig_prop size e (State.get_loc ());
+  | (Sil.Off_index e) :: off', Sil.Earray (len, esel, inst_arr), Sil.Tarray (typ', len_for_typ') ->
+      bounds_check pname orig_prop len e (State.get_loc ());
       begin
         try
           let _, se' = IList.find (fun (e', _) -> Sil.exp_equal e e') esel in
@@ -264,15 +270,19 @@ let rec _strexp_extend_values
           let replace acc (res_atoms', res_se', res_typ') =
             let replace_ise ise = if Sil.exp_equal e (fst ise) then (e, res_se') else ise in
             let res_esel' = IList.map replace_ise esel in
-            if (Sil.typ_equal res_typ' typ') || (IList.length res_esel' = 1)
-            then (res_atoms', Sil.Earray(size, res_esel', inst_arr), Sil.Tarray(res_typ', size_for_typ')) :: acc
-            else raise (Exceptions.Bad_footprint __POS__) in
+            if (Sil.typ_equal res_typ' typ') || (IList.length res_esel' = 1) then
+              ( res_atoms'
+              , Sil.Earray (len, res_esel', inst_arr)
+              , Sil.Tarray (res_typ', len_for_typ') )
+              :: acc
+            else
+              raise (Exceptions.Bad_footprint __POS__) in
           IList.fold_left replace [] atoms_se_typ_list'
         with Not_found ->
           array_case_analysis_index pname tenv orig_prop
             footprint_part kind max_stamp
-            size esel
-            size_for_typ' typ'
+            len esel
+            len_for_typ' typ'
             e off' inst_arr inst
       end
   | _, _, _ ->
@@ -280,8 +290,8 @@ let rec _strexp_extend_values
 
 and array_case_analysis_index pname tenv orig_prop
     footprint_part kind max_stamp
-    array_size array_cont
-    typ_array_size typ_cont
+    array_len array_cont
+    typ_array_len typ_cont
     index off inst_arr inst
   =
   let check_sound t' =
@@ -290,13 +300,13 @@ and array_case_analysis_index pname tenv orig_prop
   let index_in_array =
     IList.exists (fun (i, _) -> Prover.check_equal Prop.prop_emp index i) array_cont in
   let array_is_full =
-    match array_size with
+    match array_len with
     | Sil.Const (Sil.Cint n') -> Sil.Int.geq (Sil.Int.of_int (IList.length array_cont)) n'
     | _ -> false in
 
   if index_in_array then
-    let array_default = Sil.Earray(array_size, array_cont, inst_arr) in
-    let typ_default = Sil.Tarray(typ_cont, typ_array_size) in
+    let array_default = Sil.Earray (array_len, array_cont, inst_arr) in
+    let typ_default = Sil.Tarray (typ_cont, typ_array_len) in
     [([], array_default, typ_default)]
   else if !Config.footprint then begin
     let atoms, elem_se, elem_typ =
@@ -304,8 +314,8 @@ and array_case_analysis_index pname tenv orig_prop
         pname tenv orig_prop footprint_part kind max_stamp typ_cont off inst in
     check_sound elem_typ;
     let cont_new = IList.sort Sil.exp_strexp_compare ((index, elem_se):: array_cont) in
-    let array_new = Sil.Earray(array_size, cont_new, inst_arr) in
-    let typ_new = Sil.Tarray(elem_typ, typ_array_size) in
+    let array_new = Sil.Earray (array_len, cont_new, inst_arr) in
+    let typ_new = Sil.Tarray (elem_typ, typ_array_len) in
     [(atoms, array_new, typ_new)]
   end
   else begin
@@ -317,8 +327,8 @@ and array_case_analysis_index pname tenv orig_prop
             pname tenv orig_prop footprint_part kind max_stamp typ_cont off inst in
         check_sound elem_typ;
         let cont_new = IList.sort Sil.exp_strexp_compare ((index, elem_se):: array_cont) in
-        let array_new = Sil.Earray(array_size, cont_new, inst_arr) in
-        let typ_new = Sil.Tarray(elem_typ, typ_array_size) in
+        let array_new = Sil.Earray (array_len, cont_new, inst_arr) in
+        let typ_new = Sil.Tarray (elem_typ, typ_array_len) in
         [(atoms, array_new, typ_new)]
       end in
     let rec handle_case acc isel_seen_rev = function
@@ -330,10 +340,10 @@ and array_case_analysis_index pname tenv orig_prop
           let atoms_se_typ_list' =
             IList.fold_left (fun acc' (atoms', se', typ') ->
                 check_sound typ';
-                let atoms_new = Sil.Aeq(index, i) :: atoms' in
+                let atoms_new = Sil.Aeq (index, i) :: atoms' in
                 let isel_new = list_rev_and_concat isel_seen_rev ((i, se'):: isel_unseen) in
-                let array_new = Sil.Earray(array_size, isel_new, inst_arr) in
-                let typ_new = Sil.Tarray(typ', typ_array_size) in
+                let array_new = Sil.Earray (array_len, isel_new, inst_arr) in
+                let typ_new = Sil.Tarray (typ', typ_array_len) in
                 (atoms_new, array_new, typ_new):: acc'
               ) [] atoms_se_typ_list in
           let acc_new = atoms_se_typ_list' :: acc in
@@ -927,7 +937,7 @@ let type_at_offset texp off =
                (IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') instance_fields) in
            strip_offset off' typ'
          with Not_found -> None)
-    | (Sil.Off_index _):: off', Sil.Tarray (typ', _) ->
+    | (Sil.Off_index _) :: off', Sil.Tarray (typ', _) ->
         strip_offset off' typ'
     | _ -> None in
   match texp with
diff --git a/infer/src/backend/serialization.ml b/infer/src/backend/serialization.ml
index fa3c892d4..ccce64d7a 100644
--- a/infer/src/backend/serialization.ml
+++ b/infer/src/backend/serialization.ml
@@ -26,7 +26,7 @@ let tenv_key, summary_key, cfg_key, trace_key, cg_key,
   799050016, 579094948, 972393003
 
 (** version of the binary files, to be incremented for each change *)
-let version = 24
+let version = 25
 
 
 (** Retry the function while an exception filtered is thrown,
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index cdd24e782..6904c7ec0 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -170,11 +170,11 @@ let rec apply_offlist
       pp_error();
       assert false
 
-  | (Sil.Off_index idx):: offlist', Sil.Earray (size, esel, inst1) ->
+  | (Sil.Off_index idx) :: offlist', Sil.Earray (len, esel, inst1) ->
       let nidx = Prop.exp_normalize_prop p idx in
       begin
         let typ' = Tenv.expand_type tenv typ in
-        let t', size' = match typ' with Sil.Tarray (t', size') -> (t', size') | _ -> assert false in
+        let t', len' = match typ' with Sil.Tarray (t', len') -> (t', len') | _ -> assert false in
         try
           let idx_ese', se' = IList.find (fun ese -> Prover.check_equal p nidx (fst ese)) esel in
           let res_e', res_se', res_t', res_pred_insts_op' =
@@ -185,8 +185,8 @@ let rec apply_offlist
             if Sil.exp_equal idx_ese' (fst ese)
             then (idx_ese', res_se')
             else ese in
-          let res_se = Sil.Earray(size, IList.map replace_ese esel, inst1) in
-          let res_t = Sil.Tarray(res_t', size') in
+          let res_se = Sil.Earray (len, IList.map replace_ese esel, inst1) in
+          let res_t = Sil.Tarray (res_t', len') in
           (res_e', res_se, res_t, res_pred_insts_op')
         with Not_found ->
           (* return a nondeterministic value if the index is not found after rearrangement *)
@@ -264,9 +264,9 @@ let rec execute_nullify_se = function
   | Sil.Estruct (fsel, _) ->
       let fsel' = IList.map (fun (fld, se) -> (fld, execute_nullify_se se)) fsel in
       Sil.Estruct (fsel', Sil.inst_nullify)
-  | Sil.Earray (size, esel, _) ->
+  | Sil.Earray (len, esel, _) ->
       let esel' = IList.map (fun (idx, se) -> (idx, execute_nullify_se se)) esel in
-      Sil.Earray (size, esel', Sil.inst_nullify)
+      Sil.Earray (len, esel', Sil.inst_nullify)
 
 (** Do pruning for conditional [if (e1 != e2) ] if [positive] is true
     and [(if (e1 == e2)] if [positive] is false *)
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 52daf6af2..52c12a5ac 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -413,8 +413,8 @@ let rec sexp_set_inst inst = function
       Sil.Eexp (e, inst)
   | Sil.Estruct (fsel, _) ->
       Sil.Estruct ((IList.map (fun (f, se) -> (f, sexp_set_inst inst se)) fsel), inst)
-  | Sil.Earray (size, esel, _) ->
-      Sil.Earray (size, IList.map (fun (e, se) -> (e, sexp_set_inst inst se)) esel, inst)
+  | Sil.Earray (len, esel, _) ->
+      Sil.Earray (len, IList.map (fun (e, se) -> (e, sexp_set_inst inst se)) esel, inst)
 
 let rec fsel_star_fld fsel1 fsel2 = match fsel1, fsel2 with
   | [], fsel2 -> fsel2
@@ -447,11 +447,11 @@ and sexp_star_fld se1 se2 : Sil.strexp =
   match se1, se2 with
   | Sil.Estruct (fsel1, _), Sil.Estruct (fsel2, inst2) ->
       Sil.Estruct (fsel_star_fld fsel1 fsel2, inst2)
-  | Sil.Earray (size1, esel1, _), Sil.Earray (_, esel2, inst2) ->
-      Sil.Earray (size1, esel_star_fld esel1 esel2, inst2)
-  | Sil.Eexp (_, inst1), Sil.Earray (size2, esel2, _) ->
+  | Sil.Earray (len1, esel1, _), Sil.Earray (_, esel2, inst2) ->
+      Sil.Earray (len1, esel_star_fld esel1 esel2, inst2)
+  | Sil.Eexp (_, inst1), Sil.Earray (len2, esel2, _) ->
       let esel1 = [(Sil.exp_zero, se1)] in
-      Sil.Earray (size2, esel_star_fld esel1 esel2, inst1)
+      Sil.Earray (len2, esel_star_fld esel1 esel2, inst1)
   | _ ->
       L.d_str "cannot star ";
       Sil.d_sexp se1; L.d_str " and "; Sil.d_sexp se2;
diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml
index d17be4aba..623f870c6 100644
--- a/infer/src/clang/cTrans_utils.ml
+++ b/infer/src/clang/cTrans_utils.ml
@@ -684,7 +684,7 @@ let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero =
         let exp_types = zip lh_exprs lh_types in
         IList.map (fun (e, t) ->
             IList.flatten (var_or_zero_in_init_list' e t tns)) exp_types
-    | Sil.Tarray (arrtyp, Sil.Const (Sil.Cint n)) ->
+    | Sil.Tarray (arrtyp, Some n) ->
         let size = Sil.Int.to_int n in
         let indices = list_range 0 (size - 1) in
         let index_constants =
diff --git a/infer/src/clang/cType_to_sil_type.ml b/infer/src/clang/cType_to_sil_type.ml
index e988583f5..4ebdfaff5 100644
--- a/infer/src/clang/cType_to_sil_type.ml
+++ b/infer/src/clang/cType_to_sil_type.ml
@@ -61,10 +61,10 @@ let pointer_attribute_of_objc_attribute attr_info =
   | `OCL_Weak -> Sil.Pk_objc_weak
   | `OCL_Autoreleasing -> Sil.Pk_objc_autoreleasing
 
-let rec build_array_type translate_decl tenv type_ptr n =
+let rec build_array_type translate_decl tenv type_ptr n_opt =
   let array_type = type_ptr_to_sil_type translate_decl tenv type_ptr in
-  let exp = Sil.exp_int (Sil.Int.of_int64 (Int64.of_int n)) in
-  Sil.Tarray (array_type, exp)
+  let len = Option.map (fun n -> Sil.Int.of_int64 (Int64.of_int n)) n_opt in
+  Sil.Tarray (array_type, len)
 
 and sil_type_of_attr_type translate_decl tenv type_info attr_info =
   match type_info.Clang_ast_t.ti_desugared_type with
@@ -96,9 +96,9 @@ and sil_type_of_c_type translate_decl tenv c_type =
   | IncompleteArrayType (_, type_ptr)
   | DependentSizedArrayType (_, type_ptr)
   | VariableArrayType (_, type_ptr) ->
-      build_array_type translate_decl tenv type_ptr (-1)
+      build_array_type translate_decl tenv type_ptr None
   | ConstantArrayType (_, type_ptr, n) ->
-      build_array_type translate_decl tenv type_ptr n
+      build_array_type translate_decl tenv type_ptr (Some n)
   | FunctionProtoType _
   | FunctionNoProtoType _ ->
       Sil.Tfun false
diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml
index 3ff4ee7db..a7c72e7e2 100644
--- a/infer/src/eradicate/typeCheck.ml
+++ b/infer/src/eradicate/typeCheck.ml
@@ -124,7 +124,6 @@ module ComplexExpressions = struct
           case_not_handled ()
       | Sil.Dunop (op, de) ->
           Sil.str_unop op ^ dexp_to_string de
-
       | Sil.Dsizeof _ ->
           case_not_handled ()
       | Sil.Dunknown ->
@@ -528,7 +527,7 @@ let typecheck_instr
         (typecheck_expr_simple typestate' e' typ TypeOrigin.ONone loc)
         typestate'
   | Sil.Call ([id], Sil.Const (Sil.Cfun pn), [(array_exp, t)], loc, _)
-    when Procname.equal pn ModelBuiltins.__get_array_size ->
+    when Procname.equal pn ModelBuiltins.__get_array_length ->
       let (_, ta, _) = typecheck_expr
           find_canonical_duplicate
           calls_this
diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml
index 362711485..d2277edf2 100644
--- a/infer/src/harness/inhabit.ml
+++ b/infer/src/harness/inhabit.ml
@@ -84,10 +84,10 @@ let rec inhabit_typ typ cfg env =
   try (TypMap.find typ env.cache, env)
   with Not_found ->
     let inhabit_internal typ env = match typ with
-      | 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 (Some arr_size) typ ModelBuiltins.__new_array env
+      | Sil.Tptr (Sil.Tarray (inner_typ, Some _), Sil.Pk_pointer) ->
+          let len = Sil.Const (Sil.Cint (Sil.Int.one)) in
+          let arr_typ = Sil.Tarray (inner_typ, Some Sil.Int.one) in
+          inhabit_alloc arr_typ (Some len) 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) *)
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index dd54191be..67e91b6ff 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -400,8 +400,8 @@ let use_static_final_fields context =
 let builtin_new =
   Sil.Const (Sil.Cfun ModelBuiltins.__new)
 
-let builtin_get_array_size =
-  Sil.Const (Sil.Cfun ModelBuiltins.__get_array_size)
+let builtin_get_array_length =
+  Sil.Const (Sil.Cfun ModelBuiltins.__get_array_length)
 
 let create_sil_deref exp typ loc =
   let fresh_id = Ident.create_fresh Ident.knormal in
@@ -447,7 +447,8 @@ let rec expression context pc expr =
             let deref = create_sil_deref sil_ex array_typ_no_ptr loc in
             let args = [(sil_ex, type_of_ex)] in
             let ret_id = Ident.create_fresh Ident.knormal in
-            let call_instr = Sil.Call([ret_id], builtin_get_array_size, args, loc, Sil.cf_default) in
+            let call_instr =
+              Sil.Call ([ret_id], builtin_get_array_length, args, loc, Sil.cf_default) in
             (instrs @ [deref; call_instr], Sil.Var ret_id, type_of_expr)
         | JBir.Conv conv ->
             let cast_ex = Sil.Cast (JTransType.cast_type conv, sil_ex) in
@@ -478,7 +479,7 @@ let rec expression context pc expr =
         match binop with
         | JBir.ArrayLoad _ ->
             (* add an instruction that dereferences the array *)
-            let array_typ = Sil.Tarray(type_of_expr, Sil.Var (Ident.create_fresh Ident.kprimed)) in
+            let array_typ = Sil.Tarray (type_of_expr, None) in
             let deref_array_instr = create_sil_deref sil_ex1 array_typ loc in
             let id = Ident.create_fresh Ident.knormal in
             let letderef_instr =
@@ -638,17 +639,17 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
 
   (callee_procname, instrs)
 
-let get_array_size context pc expr_list content_type =
+let get_array_length context pc expr_list content_type =
   let get_expr_instr expr other_instrs =
-    let (instrs, sil_size_expr, _) = expression context pc expr in
+    let (instrs, sil_len_expr, _) = expression context pc expr in
     match other_instrs with
     | (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_len sil_size_expr (content_type, _) =
-    (Sil.Tarray (content_type, sil_size_expr), Some sil_size_expr) in
+        (instrs @ other_instrs, sil_len_expr :: other_exprs) in
+  let (instrs, sil_len_exprs) = (IList.fold_right get_expr_instr expr_list ([],[])) in
+  let get_array_type_len sil_len_expr (content_type, _) =
+    (Sil.Tarray (content_type, None), Some sil_len_expr) in
   let array_type, array_len =
-    IList.fold_right get_array_type_len sil_size_exprs (content_type, None) in
+    IList.fold_right get_array_type_len sil_len_exprs (content_type, None) in
   let array_size = Sil.Sizeof (array_type, array_len, Sil.Subtype.exact) in
   (instrs, array_size)
 
@@ -925,7 +926,7 @@ let rec instruction context pc instr : translation =
         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
-        let (instrs, array_size) = get_array_size context pc expr_list content_type in
+        let (instrs, array_size) = get_array_length context pc expr_list content_type in
         let call_args = [(array_size, array_type)] in
         let ret_id = Ident.create_fresh Ident.knormal in
         let call_instr = Sil.Call([ret_id], builtin_new_array, call_args, loc, Sil.cf_default) in
diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml
index ac206d62f..be6bed99f 100644
--- a/infer/src/java/jTransType.ml
+++ b/infer/src/java/jTransType.ml
@@ -69,8 +69,7 @@ let rec get_named_type vt =
         match ot with
         | JBasics.TArray vt ->
             let content_type = get_named_type vt in
-            let size = Sil.exp_get_undefined false in
-            Sil.Tptr (Sil.Tarray (content_type, size), Sil.Pk_pointer) (* unknown size *)
+            Sil.Tptr (Sil.Tarray (content_type, None), Sil.Pk_pointer)
         | JBasics.TClass cn -> Sil.Tptr (Sil.Tvar (typename_of_classname cn), Sil.Pk_pointer)
       end
 
@@ -84,8 +83,7 @@ let extract_cn_type_np typ =
 let rec create_array_type typ dim =
   if dim > 0 then
     let content_typ = create_array_type typ (dim - 1) in
-    let size = Sil.exp_get_undefined false in
-    Sil.Tptr(Sil.Tarray (content_typ, size), Sil.Pk_pointer)
+    Sil.Tptr(Sil.Tarray (content_typ, None), Sil.Pk_pointer)
   else typ
 
 let extract_cn_no_obj typ =
@@ -384,9 +382,7 @@ let is_closeable program tenv typ =
 let rec object_type program tenv ot =
   match ot with
   | JBasics.TClass cn -> get_class_type program tenv cn
-  | JBasics.TArray at ->
-      let size = Sil.exp_get_undefined false in
-      Sil.Tptr (Sil.Tarray (value_type program tenv at, size), Sil.Pk_pointer)
+  | JBasics.TArray at -> Sil.Tptr (Sil.Tarray (value_type program tenv at, None), Sil.Pk_pointer)
 (** translate a value type *)
 and value_type program tenv vt =
   match vt with
@@ -397,9 +393,6 @@ 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, len), Sil.Pk_pointer) ->
-      let typ = (Sil.Tarray (vtyp, len)) in
-      Sil.Sizeof (typ, Some len, subtypes)
   | Sil.Tptr (typ, _) ->
       Sil.Sizeof (typ, None, subtypes)
   | _ ->
diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml
index 336205238..97be414b6 100644
--- a/infer/src/llvm/lTrans.ml
+++ b/infer/src/llvm/lTrans.ml
@@ -36,7 +36,7 @@ let rec trans_typ : LAst.typ -> Sil.typ = function
   | Tfloat -> Sil.Tfloat Sil.FFloat
   | Tptr tp -> Sil.Tptr (trans_typ tp, Sil.Pk_pointer)
   | Tvector (i, tp)
-  | Tarray (i, tp) -> Sil.Tarray (trans_typ tp, Sil.Const (Sil.Cint (Sil.Int.of_int i)))
+  | Tarray (i, tp) -> Sil.Tarray (trans_typ tp, Some (Sil.Int.of_int i))
   | Tfunc _ -> Sil.Tfun false
   | Tlabel -> raise (ImproperTypeError "Tried to generate Sil type from LLVM label type.")
   | Tmetadata -> raise (ImproperTypeError "Tried to generate Sil type from LLVM metadata type.")
diff --git a/infer/tests/endtoend/java/tracing/ArrayIndexOutOfBoundsExceptionTest.java b/infer/tests/endtoend/java/tracing/ArrayIndexOutOfBoundsExceptionTest.java
index db8092e3c..84a3f1ab2 100644
--- a/infer/tests/endtoend/java/tracing/ArrayIndexOutOfBoundsExceptionTest.java
+++ b/infer/tests/endtoend/java/tracing/ArrayIndexOutOfBoundsExceptionTest.java
@@ -42,9 +42,8 @@ public class ArrayIndexOutOfBoundsExceptionTest {
   public void matchErrors()
       throws IOException, InterruptedException, InferException {
     String[] methods = {
-//        TODO (#7651424): re-enable these tests once the translation of arrays is fixed
-//        "callOutOfBound",
-//        "missingCheckOnIndex",
+       "callOutOfBound",
+       "missingCheckOnIndex",
         "arrayIndexOutOfBoundsInCallee",
     };
     assertThat(