Frama-C news and ideas

Here are two links related to ptrdiff_t:

• Ptrdiff_t is evil, a blog post for if you are not tired of conversion and promotion issues yet,
• and an interesting answer on StackOverflow.

I was doubtful about the second one (I had no difficulties to accept the first one after the previous conversions-and-promotions-related posts on this blog). But type ptrdiff_t is for storing pointer differences, right? Why would a compilation platform (compiler and associated standard library including malloc()) make it just too small to hold all possible pointer differences? So I tested it, and StackOverflow user R.. is right:

#include <stddef.h>
#include <stdio.h>

main(){
  printf("%d\n", (int) sizeof(ptrdiff_t));
}

Compiling as a 32-bit program:

$ gcc -m32 t.c && ./a.out 
4

I am pretty sure I have allocated 2.2GB in a single malloc() call of a 32-bit process on this system. I was thankful for getting that much at the time, too. But 4 bytes are not enough to hold all signed differences between two pointers to char within a single 2.2GB chunk of memory:

#include <stdio.h>
#include <stdlib.h>

main(){
  char *p = malloc(2200000000U);
  if (!p) return 1;
  char *q = p + 2150000000U;
  printf("%td\n", q - p);
}

Please take a moment to predict the number printed by the above program yourself before looking down.

$ gcc -m32 t.c && ./a.out 
-2144967296