test from Dan

Author: Daniel Kroening

regression/cbmc/Pointer_array4/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int arrayOfIntegers[] = {1, 2, 3};
+  int *pointer2FirstElem = arrayOfIntegers;
+  int *pointer2ThirdElem = arrayOfIntegers + 2;
+  int iFirst=(int)pointer2FirstElem;
+  int iThird=(int)pointer2ThirdElem;
+  int addrDiff = iThird-iFirst;
+  assert(addrDiff == 2* sizeof(int));
+  return 0;
+}

regression/cbmc/Pointer_array4/test.desc

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