Changeset 1030 for src/ASM/CPP2011


Ignore:
Timestamp:
Jun 21, 2011, 2:24:35 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r1029 r1030  
    575575However, this comes at the expense of assembler completeness: the generated program may be too large to fit into code memory.
    576576In this respect, there is a trade-off between the completeness of the assembler and the efficiency of the assembled program.
    577 The definition and proof of a complete, optimal (in the sense that jump pseudoinstructions are expanded to the smallest possible opcode) and correct jump expansion policy is ongoing work.
     577The definition and proof of a complete, optimal (in the sense that object code size is minimized) and correct jump expansion policy is ongoing work.
    578578
    579579Aside from their application in verified compiler projects such as CerCo and CompCert, verified assemblers such as ours could also be applied to the verification of operating system kernels.
Note: See TracChangeset for help on using the changeset viewer.