Merge pull request #228 from smowton/fix_typecast_array_access

Fix typecast array access

Author: Daniel Kroening

regression/cbmc-java/arrayread1/arrayread1.class

@@ -0,0 +1,14 @@
+public class arrayread1 {
+
+  static arrayread1 readback;
+
+  public static void main(int c) {
+
+    if(c!=1) return;
+    arrayread1[] a = new arrayread1[c];
+    readback=a[0];
+    assert(readback==null);
+
+  }
+
+}

regression/cbmc-java/arrayread1/arrayread1.java

@@ -0,0 +1,8 @@
+CORE
+arrayread1.class
+--unwind 3 --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/arrayread1/test.desc

@@ -296,7 +296,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     const typet &op_type=ns.follow(op.type());
 
     if(op_type.id()==ID_pointer)
-      return convert_pointer_type(op);
+      return convert_bv(op);
     else if(op_type.id()==ID_signedbv ||
             op_type.id()==ID_unsignedbv ||
             op_type.id()==ID_bool ||