/* convert double to IEEE 32 bit floating number and vice versa
   (denormalized numbers are considered as zero) */

void double2ieee(double input, char ieee[4]);
double ieee2double(char ieee[4]);