+ return (a * uchar_s * uchar_s * uchar_s) + (b * uchar_s * uchar_s) + (c * uchar_s) + d; }
+
+extern void write_uint16_bigendian(uint16_t x, FILE * file) {
+// Write uint16 to file in beg-endian order.
+ unsigned char a = x / uchar_s;
+ unsigned char b = x % uchar_s;
+ fputc(a, file);
+ fputc(b, file); }