search

seL4 / sel4test

Test suite for seL4.
http://sel4.systems
Other
25 stars 63 forks source link

aarch64: Use 32-bit sized register names #92

Closed kent-mcleod closed 1 year ago

kent-mcleod commented 1 year ago

The fault assembly code manipulates an integer sized argument and so 32-bit register names need to be used in order to avoid compiler warnings.

axel-h commented 1 year ago

Why not simply change the type from int to word?

kent-mcleod commented 1 year ago

Why not simply change the type from int to word?

Cause x86_64 is already using 32-bit register names