Bit-level encoding of pointers may lose offset bits

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@5546 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

regression/cbmc/Pointer_Arithmetic13/main.c

@@ -0,0 +1,22 @@
+// simplified version of openbsd_cmemrchr-alloca_true-valid-memsafety.i
+
+int main() {
+  long n;
+  __CPROVER_assume(n>=1);
+
+  char X;
+  char* s = &X;
+
+  const char *cp;
+  cp = s + n; // loses high bits of n for any bits above offset_bits
+
+  //long cp_l=(long)cp;
+  //long s_l=(long)s;
+  //long n_l=(long)n;
+  //long s_n=(long)s+n;
+
+  __CPROVER_assert((long)cp == (long)s + n, "");
+
+  return 0;
+}
+

regression/cbmc/Pointer_Arithmetic13/test.desc

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