diff options
| author | Brian Campbell | 2019-01-01 13:54:31 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-01-01 13:54:31 +0000 |
| commit | 3e311bd2a9072146f53bf6c2db9a811d38aee601 (patch) | |
| tree | 48d0db0738ef932e40deb57e168382966dd68599 /lib/coq/Sail2_instr_kinds.v | |
| parent | 534e02c863b5a571c6d8bd65cf72a4ce92fe4701 (diff) | |
Coq: update instr_kinds from Lem
Diffstat (limited to 'lib/coq/Sail2_instr_kinds.v')
| -rw-r--r-- | lib/coq/Sail2_instr_kinds.v | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v index eadc567a..c6fb866b 100644 --- a/lib/coq/Sail2_instr_kinds.v +++ b/lib/coq/Sail2_instr_kinds.v @@ -157,6 +157,7 @@ Inductive barrier_kind := | Barrier_RISCV_rw_r | Barrier_RISCV_r_w | Barrier_RISCV_w_r + | Barrier_RISCV_tso | Barrier_RISCV_i (* X86 *) | Barrier_x86_MFENCE. @@ -182,6 +183,11 @@ instance (Show barrier_kind) | Barrier_RISCV_r_r -> "Barrier_RISCV_r_r" | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" + | Barrier_RISCV_w_rw -> "Barrier_RISCV_w_rw" + | Barrier_RISCV_rw_r -> "Barrier_RISCV_rw_r" + | Barrier_RISCV_r_w -> "Barrier_RISCV_r_w" + | Barrier_RISCV_w_r -> "Barrier_RISCV_w_r" + | Barrier_RISCV_tso -> "Barrier_RISCV_tso" | Barrier_RISCV_i -> "Barrier_RISCV_i" | Barrier_x86_MFENCE -> "Barrier_x86_MFENCE" end @@ -295,8 +301,13 @@ instance (EnumerationType barrier_kind) | Barrier_RISCV_r_r -> 15 | Barrier_RISCV_rw_w -> 16 | Barrier_RISCV_w_w -> 17 - | Barrier_RISCV_i -> 18 - | Barrier_x86_MFENCE -> 19 + | Barrier_RISCV_w_rw -> 18 + | Barrier_RISCV_rw_r -> 19 + | Barrier_RISCV_r_w -> 20 + | Barrier_RISCV_w_r -> 21 + | Barrier_RISCV_tso -> 22 + | Barrier_RISCV_i -> 23 + | Barrier_x86_MFENCE -> 24 end end *) |