I took your advice and wrote some code to generate that. The exercise was not futile. I had mistakenly thought I couldn't set the sign bit using hex notation, but now I know. I must have misinterpreted the warning about 64-bit hex being non-portable.