do_load_word
u_int32_t do_load_word(vaddr_t, int);
v = do_load_word(dmax, dmtx & DMT_DAS);
v = do_load_word(dmax ^ 4, dmtx & DMT_DAS);
v = do_load_word(dmax, dmtx & DMT_DAS);
((u_int32_t *)(do_load_word))[1] = 0xf400c401;