test for issue #188

Author: Daniel Kroening

regression/cbmc/Pointer_array5/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stdlib.h>
+
+extern int nondet_int();
+
+int main() {
+
+  int arraylen=nondet_int();
+
+  if(arraylen==3)
+  {
+    int** array_init = malloc(sizeof(int *)*arraylen);
+
+    int a0, a1, a2;
+
+    array_init[0] = &a0;
+    array_init[1] = &a1;
+    array_init[2] = &a2;
+
+    void **local_array=(void**)array_init;
+    
+    int *address=(int *)local_array[0];
+    assert(address==&a0);
+  }
+
+}

regression/cbmc/Pointer_array5/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring