diff options
| author | Brian Campbell | 2018-08-15 13:59:16 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-15 13:59:16 +0100 |
| commit | b73f6d13b4bf2291f71616abdb046e2ca657d868 (patch) | |
| tree | e999f8ccde5f510a9c004197b7fa142c346d9982 /lib/coq/Sail2_instr_kinds.v | |
| parent | 39fea17bac77535c9cff47cd6657a308e391ac8a (diff) | |
Get RISC-V on Coq into reasonable state to show
- Fill in Coq builtins for more of the RISC-V prelude
- Update Barriers
- More general autocast
- Temporary sub_nat definition (until the backend handles nat better)
- Patch to bring results into a reasonable state
- Use Let rather than Definition for non-dependent top-level values
Diffstat (limited to 'lib/coq/Sail2_instr_kinds.v')
| -rw-r--r-- | lib/coq/Sail2_instr_kinds.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v index 57532e92..c93e9e93 100644 --- a/lib/coq/Sail2_instr_kinds.v +++ b/lib/coq/Sail2_instr_kinds.v @@ -153,6 +153,10 @@ Inductive barrier_kind := | Barrier_RISCV_r_r | Barrier_RISCV_rw_w | Barrier_RISCV_w_w + | Barrier_RISCV_w_rw + | Barrier_RISCV_rw_r + | Barrier_RISCV_r_w + | Barrier_RISCV_w_r | Barrier_RISCV_i (* X86 *) | Barrier_x86_MFENCE. |