|
Last change
on this file was
2394,
checked in by campbell, 7 years ago
|
|
I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.
|
|
File size:
799 bytes
|
| Line | |
|---|
| 1 | Ilias asked about this and I don't appear to have a note from before: |
|---|
| 2 | |
|---|
| 3 | Our pointer offsets are just bitvectors, and our memory model allows for |
|---|
| 4 | looking up negative offsets (given in Z) in memory. So do we take the |
|---|
| 5 | bitvectors to be signed or unsigned? |
|---|
| 6 | |
|---|
| 7 | They must be unsigned, because we can have offsets > 2^{15}, e.g., by |
|---|
| 8 | allocating most of the memory in a 40kB array and making a pointer to the |
|---|
| 9 | last element. We only use the pointer type to access memory in CerCo at the |
|---|
| 10 | moment, so negative offsets are inaccessible. CompCert has a similar |
|---|
| 11 | arrangement, but its memory model has a load function that takes an offset |
|---|
| 12 | in Z directly (in addition to the one that take a pointer value and can only |
|---|
| 13 | hit positive offsets), so they can access negative offsets from other parts of |
|---|
| 14 | the language semantics. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
