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.ml | |
| 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.ml')
| -rw-r--r-- | language/l2.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/language/l2.ml b/language/l2.ml index 6ce6a064..ea3252da 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -1,4 +1,4 @@ -(* generated by Ott 0.25 from: l2.ott *) +(* generated by Ott 0.24 from: l2.ott *) type text = string @@ -64,6 +64,8 @@ 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 *) |