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