7 rt
= 0x1234567887654321;
8 rs
= 0xabcd1234abcd8765;
10 res
= 0x1234567887654321;
12 ("dappend %0, %1, 0x0\n\t"
18 printf("dappend error\n");
22 rt
= 0x1234567887654321;
23 rs
= 0xabcd1234abcd8765;
25 res
= 0x2345678876543215;
27 ("dappend %0, %1, 0x4\n\t"
33 printf("dappend error\n");