Merge pull request #1013 from smowton/smowton/fix/array_of_zero_length

Don't warn on array_of_expr with zero length

Author: Daniel Kroening

regression/cbmc-java/array2/test.class

@@ -0,0 +1,6 @@
+CORE
+test.class
+--function test.f --cover location
+\d+ of \d+ covered
+--
+^warning: ignoring

regression/cbmc-java/array2/test.desc

@@ -0,0 +1,16 @@
+public class test {
+
+  public void f(int unknown) {
+
+    int[] arr;
+    if(unknown > 0)
+      arr = new int[1];
+    else
+      arr = new int[0];
+
+    if(unknown > 0)
+      arr[0]=1;
+
+  }
+
+}

regression/cbmc-java/array2/test.java

@@ -25,7 +25,14 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
   std::size_t width=boolbv_width(array_type);
 
   if(width==0)
-    return conversion_failed(expr);
+  {
+    // A zero-length array is acceptable;
+    // an element with unknown size is not.
+    if(boolbv_width(array_type.subtype())==0)
+      return conversion_failed(expr);
+    else
+      return bvt();
+  }
 
   const exprt &array_size=array_type.size();
 

src/solvers/flattening/boolbv_array_of.cpp

@@ -37,7 +37,13 @@ bvt boolbvt::convert_with(const exprt &expr)
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
-    return conversion_failed(expr);
+  {
+    // A zero-length array is acceptable:
+    if(expr.type().id()==ID_array && boolbv_width(expr.type().subtype())!=0)
+      return bvt();
+    else
+      return conversion_failed(expr);
+  }
 
   if(bv.size()!=width)
   {