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 user 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 an 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