• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Introduction
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
        • Implemented-opcodes
        • Proof-utilities
        • To-do
          • Concrete-simulation-examples
          • Model-validation
          • Utils
          • Debugging-code-proofs
        • Execloader
        • Axe
      • Testing-utilities
      • Math
    • X86isa

    To-do

    Known issues, planned activities, wishlists, etc.

    If anyone is interested in carrying out the tasks or activities below, please feel free to contact Shilpi (shigoel@cs.utexas.edu).

    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.
    • Verify guards of functions in tools/execution/exec-loaders/elf/.
    • Add support for exception handling. Currently the occurence of an exception in the model just stores some information in the x86 state stobj, and the step function does nothing when that information is present.

    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.