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