Tiens, je viens de voir une autre différence entre les stdint.h de TIGCC et GCC4TI: dans GCC4TI, nous avons fait le choix de suivre C99+TC1+TC2 (paragraphe 7.18.2) pour les valeurs de INT*_MIN, INT_FAST*_MIN, INT_LEAST*_MIN et INTMAX_MIN. A savoir, que la valeur -2^(N-1) n'est pas autorisée, aussi bizarre que ça paraisse.
Même remarque pour INTPTR_MIN, si ce n'est que TIGCC et GCC4TI ont tous les deux étendu la plage à 32 bits (une plage de 16 bits, quand les pointeurs font plus de 16 bits, paraît bizarre).

Qu'est-ce qu'on fait ?