docs: @Ensures({
      "!allowEOF ? result >= 0 : result >= -1"
    })
    protected int readChar(boolean allowEOF) throws IOException {
      int c = reader.read();
      if (c != -1) {
        ++currentOffset;
      } else {
        if (!allowEOF) {
          throw new IOException();
        }
      }
      return c;
    }