diff options
| author | Kathy Gray | 2015-06-24 15:34:14 +0100 |
|---|---|---|
| committer | Kathy Gray | 2015-06-24 15:34:14 +0100 |
| commit | 44290b8b62f118bfd6f1b6da01f850cfc2816cbb (patch) | |
| tree | 54d685a281ee23d005e9f0ddd83004e2af0a5b8c /language/l2.lem | |
| parent | a947fe25f647fe83f6ec24599173c61eaa342ea1 (diff) | |
Support new memory write events in the sail front end and pretty printer
Events are eamem to signal the memory address to write to and wmv to pass the value to write
Diffstat (limited to 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/language/l2.lem b/language/l2.lem index adbb38b6..36d64694 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -1,4 +1,4 @@ -(* generated by Ott 0.25 from: l2_typ.ott l2.ott *) +(* generated by Ott 0.24 from: l2_typ.ott l2.ott *) open import Pervasives open import Map @@ -67,6 +67,8 @@ type base_effect_aux = (* effect *) | BE_wreg (* write register *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) + | BE_eamem (* signal effective address for writing memory *) + | BE_wmv (* write memory, sending only value *) | BE_barr (* memory barrier *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) |