#include <stdint.h>
#define PTRDIFF_MAX                                   /* FIXME */        (65535)

/*
STDC(199901)
*/