• Robbert Krebbers's avatar
    More lenient pointer equality. · 914f32ee
    Robbert Krebbers authored
    Pointer equality is now defined using absolute object offsets. The treatment
    is similar to CompCert:
    * Equality of pointers in the same object is defined provided the object has
      not been deallocated.
    * Equality of pointers in different objects is defined provided both pointers
      have not been deallocated and both are strict (i.e. not end-of-array).
    Thus, pointer equality is defined for all pointers that are not-end-of-array
    and have not been deallocated. The following examples have defined behavior:
      int x, y;
      printf("%d\n", &x == &y);
      int *p = malloc(sizeof(int)), *q = malloc(sizeof(int));
      printf("%d\n", p == q);
      struct S { int a; int b; } s, *r = &s;
      printf("%d\n", &s.a + 1 == &(r->b));
    The following not:
      int x, y;
      printf("%d\n", &x + 1 == &y);
decidable.v 9.02 KB