Merge pull request diffblue#4711 from tautschnig/empty-array

Fix segmentation fault with empty array

Author: tautschnig

regression/cbmc/array-tests/zero-sized.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int A[0] = {};
+  int i;
+  if(A[i] == 1)
+    __CPROVER_assert(0, "");
+}

regression/cbmc/array-tests/zero-sized.desc

@@ -0,0 +1,8 @@
+CORE
+zero-sized.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/solvers/flattening/boolbv_index.cpp

@@ -124,6 +124,11 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       symbol_exprt result(identifier, expr.type());
       bv = convert_bv(result);
 
+      // return an unconstrained value in case of an empty array (the access is
+      // necessarily out-of-bounds)
+      if(!array.has_operands())
+        return bv;
+
       equal_exprt value_equality(result, array.op0());
 
       binary_relation_exprt lower_bound(