Commit 07674eec authored by Hai Dang's avatar Hai Dang

quote Miri implemention in README

parent b3668f02
...@@ -90,19 +90,19 @@ The directory structure is as follows. ...@@ -90,19 +90,19 @@ The directory structure is as follows.
[lang/bor_semantics.v](theories/lang/bor_semantics.v). The following table [lang/bor_semantics.v](theories/lang/bor_semantics.v). The following table
matches the definitions in the technical [appendix] with the Coq definitions and their [Miri implementation][Implementation]. matches the definitions in the technical [appendix] with the Coq definitions and their [Miri implementation][Implementation].
| Definitions in [appendix] | Coq definitions in `bor_semantics.v` | [Implementation] in Miri | | Definitions in [appendix] | Coq definitions in `bor_semantics.v` | [Implementation] in Miri |
|--------------------------------|--------------------------------------|--------------------------| |--------------------------------|--------------------------------------|----------------------------|
| `Grants` | `grants` | Permission::grants | | `Grants` | `grants` | `Permission::grants` |
| `FindGranting` | `find_granting` | Stack::find_granting | | `FindGranting` | `find_granting` | `Stack::find_granting` |
| `FindFirstWIncompat` | `find_first_write_incompatible` | Stack::find_first_write_incompatible | | `FindFirstWIncompat` | `find_first_write_incompatible` | `Stack::find_first_write_incompatible` |
| `Access` | `access1` | Stack::access | | `Access` | `access1` | `Stack::access` |
| `MemAccessed(_,_,AccessRead)` | `memory_read` | Stacks::memory_read | | `MemAccessed(_,_,AccessRead)` | `memory_read` | `Stacks::memory_read` |
| `MemAccessed(_,_,AccessWrite)` | `memory_written` | Stacks::memory_written | | `MemAccessed(_,_,AccessWrite)` | `memory_written` | `Stacks::memory_written` |
| `Dealloc` | `dealloc1` | Stack::dealloc | | `Dealloc` | `dealloc1` | `Stack::dealloc` |
| `MemDeallocated` | `memory_deallocated` | Stacks::memory_deallocated | | `MemDeallocated` | `memory_deallocated` | `Stacks::memory_deallocated` |
| `GrantTag` | `grant` | Stack::grant | | `GrantTag` | `grant` | `Stack::grant` |
| `Reborrow` | `reborrow` | EvalContextPrivExt::reborrow | | `Reborrow` | `reborrow` | `EvalContextPrivExt::reborrow` |
| `Retag` | `retag` | EvalContextPrivExt::retag_reference | | `Retag` | `retag` | `EvalContextPrivExt::retag_reference` |
- The complete language is then combined in [lang/lang.v](theories/lang/lang.v). - The complete language is then combined in [lang/lang.v](theories/lang/lang.v).
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment