int strintcmp (char const *, char const *)
  _GL_ATTRIBUTE_NONNULL () _GL_ATTRIBUTE_PURE;
int strnumcmp (char const *, char const *, int, int)
  _GL_ATTRIBUTE_NONNULL () _GL_ATTRIBUTE_PURE;