while($usedouble || !eof($file_in)) {
  if($usedouble) {
   $new_code=$double; $usedouble=0;
  } else {
   $r=read($file_in, $double, 3); ($double)=unpack(N,"\000$double");
   $new_code=$double & 0xfff; $double >>= 12; $usedouble=1;
  }
  # etc
 }