I knew about the standard 'e' exponent for decimal notation, but the linux man page of strtod says about the hexadecimal notation:
A hexadecimal number consists of a "0x" or "0X" followed by a nonempty sequence of hexadecimal digits possibly containing a radix character, optionally followed by a binary exponent. A binary exponent consists of a 'P' or 'p', followed by an optional plus or minus sign, followed by a nonempty sequence of decimal digits, and indicates multiplication by a power of 2. At least one of radix character and binary exponent must be present.
Playing with a C compiler: 0x0123456789ABCDEFp019
is equal to 4.2984030182685396e+22
but I cannot reimplement that successfully myself.