Application-level view of the x86 model
The x86 model can be used in the application-level view
when the value of the field
Some supervisor-level features are neither used nor required for the analysis of application software. In most cases, a application cares about the correctness of his application program while assuming that services like paging and I/O operations are provided reliably by the operating system. The application-level view of our model attempts to provide the same environment to a application for reasoning as is provided by an OS for programming. In this mode, our memory model provides the 2^48-byte linear address space specified for modern 64-bit Intel machines.
A 64-bit canonical address can be in either of the two ranges below:0 to 2^47-1 or 2^64-2^47 to 2^64-1
Note that this address space is 2^48 bytes of memory. So I can use the addresses0 to 2^47-1
to map the first range, and the addresses-2^47 to -1
to map the second range.0 to 2^47-1 | 0 to 2^47-1
The advantage of doing so is that we will avoid bignum creation during address computations.
The guards of the linear memory functions are stricter than those