source: src/Clight/test/endptr2.c @ 2771

Last change on this file since 2771 was 2395, checked in by campbell, 7 years ago

Proper handling of comparison of pointers off-the-end of an object.
We might need to drop this if the proofs/back-end work is too involved.

File size: 488 bytes
Line 
1/* C allows pointers just past the end of an object (e.g., to facilitate
2   some looping code that maintains a pointer into an array), but other
3   out of object pointers shouldn't be comparable.
4
5   This should fail with undefined behaviour.
6    */
7
8int main(void) {
9  int x,y,z;
10  int *px = &x;
11  int *px1 = &x + 1;
12  int *px2 = &x + 2;
13
14  /* This should be OK */
15  if (px < px1) {
16    /* Bad comparison, px2 may wrap around in memory */
17    if (px1 < px2) return 1;
18  }
19
20  return 1;
21}
Note: See TracBrowser for help on using the repository browser.