To-do
Known issues, planned activities, wishlists, etc.
As of 2025, the X86ISA model is being maintained and extended by
the ACL2 community. If anyone is interested in carrying out the tasks or
activities below, please feel free to contact us at
acl2-books@googlegroups.com.
TO-DO
- Remove the capability of reading and writing 6 and 10 bytes from
x86-operand-* functions, in light of alignment checking.
- Check the segmentation specification and test the far jmp
instruction.
- Add support for handling more exceptions. In the past, no exception
handling was supported. In the effort to boot Linux, we added support for page
faults, but most other exceptions are still unhandled.
Wishlist
- Save memory by loading either the elf or mach-o stobj as
necessary, as opposed to loading both by default in
tools/execution/top.lisp.
