diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2019-01-02 13:32:24 +0000 |
|---|---|---|
| committer | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2019-01-02 13:32:24 +0000 |
| commit | de21f8aeaa092e68e220829ff8c3da4132e6f8fe (patch) | |
| tree | b929a1cde3eb524e9bdcdf57649ca6b7e8677fbb | |
| parent | 2ee907495d64b11ff853a68d68929395fc38bc3b (diff) | |
| download | sail-riscv-de21f8aeaa092e68e220829ff8c3da4132e6f8fe.zip sail-riscv-de21f8aeaa092e68e220829ff8c3da4132e6f8fe.tar.gz sail-riscv-de21f8aeaa092e68e220829ff8c3da4132e6f8fe.tar.bz2 | |
Add missing Coq TSO built-in
| -rw-r--r-- | riscv_extras.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/riscv_extras.v b/riscv_extras.v index 6de320d..ff235a9 100644 --- a/riscv_extras.v +++ b/riscv_extras.v @@ -18,6 +18,7 @@ Definition MEM_fence_w_rw {rv e} (_:unit) : monad rv unit e := barrier Barrier_ Definition MEM_fence_rw_r {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_rw_r. Definition MEM_fence_r_w {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_r_w. Definition MEM_fence_w_r {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_w_r. +Definition MEM_fence_tso {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_tso. Definition MEM_fence_i {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_i. (* val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e |