#ifdef NEED_DRAND48
double drand48(void);
#endif