• 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);
    914f32ee
decidable.v 9.02 KB