svoid bytesToChars_bigEndian(byte[] a, char[] b) {
  int n = l(a)/2;
  for i to n:
    b[i] = (char) (((int) a[i]) << 8 | ((int) a[i+1]) & 0xFF);
}