void load_32bit_constant(void)
{
    volatile unsigned long c = 0x12345678;
}