From 229ca26c8b2f06c939f9464107bb218fd2675f26 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 8 Jun 2016 10:38:04 -0700
Subject: [PATCH] Optimize normalization, substitution, renaming of array types

Summary:
Array types where the length is not statically known were represented
using fresh variables.  This diff:

- Makes array type length optional, reducing the amount of work needed
  for renaming, substitution, and normalization.

- Revises uses of array length so that the length component of a
  Tarray type represents only the statically determined constant
  length of an array type, and the length component of a Sizeof
  expression represents the dynamically determined length of an array
  value.

- Restricts the type of static lengths from a general expression
  (Sil.exp) to an integer (Sil.Int.t), enforcing that static types are
  constant.  This in particular ensures that types contain no
  variables, and so are invariant under operations such as renaming
  and substitution.

- Removes the type substitution and renaming functions typ_sub,
  typ_normalize, and typ_captured_ren.  Now that array type lengths
  are constant integers, all of these functions are the identity.

Reviewed By: cristianoc

Differential Revision: D3387343

fbshipit-source-id: b5db768
---
 infer/models/c/src/glib.c                     |   4 +-
 infer/models/c/src/infer_builtins.h           |   4 +-
 infer/models/c/src/libc_basic.c               |  64 +++----
 infer/models/c/src/wchar.c                    |   2 +-
 .../models/objc/src/CoreFoundation/CFString.c |   4 +-
 infer/models/objc/src/NSString.m              |   4 +-
 infer/src/IR/Sil.re                           | 116 ++++++------
 infer/src/IR/Sil.rei                          |  24 ++-
 infer/src/IR/Tenv.re                          |   3 +-
 infer/src/backend/abs.ml                      |   6 +-
 infer/src/backend/absarray.ml                 |  26 +--
 infer/src/backend/autounit.ml                 |  14 +-
 infer/src/backend/dom.ml                      |  93 +++++-----
 infer/src/backend/dotty.ml                    |  12 +-
 infer/src/backend/iList.ml                    |   4 +-
 infer/src/backend/iList.mli                   |   4 +-
 infer/src/backend/match.ml                    |   8 +-
 infer/src/backend/modelBuiltins.ml            |  84 ++++-----
 infer/src/backend/modelBuiltins.mli           |   4 +-
 infer/src/backend/prop.ml                     | 172 +++++-------------
 infer/src/backend/prover.ml                   | 108 ++++++-----
 infer/src/backend/rearrange.ml                | 144 ++++++++-------
 infer/src/backend/serialization.ml            |   2 +-
 infer/src/backend/symExec.ml                  |  12 +-
 infer/src/backend/tabulation.ml               |  12 +-
 infer/src/clang/cTrans_utils.ml               |   2 +-
 infer/src/clang/cType_to_sil_type.ml          |  10 +-
 infer/src/eradicate/typeCheck.ml              |   3 +-
 infer/src/harness/inhabit.ml                  |   8 +-
 infer/src/java/jTrans.ml                      |  25 +--
 infer/src/java/jTransType.ml                  |  13 +-
 infer/src/llvm/lTrans.ml                      |   2 +-
 .../ArrayIndexOutOfBoundsExceptionTest.java   |   5 +-
 33 files changed, 469 insertions(+), 529 deletions(-)

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(