diff options
| author | Brian Campbell | 2018-09-05 16:44:44 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-09-06 17:57:23 +0100 |
| commit | 4e2d59f0af54d316ec343d02f25a065bcff259f8 (patch) | |
| tree | 764caab9829340153a2a2381260ef1bbe1574b3d /lib/coq/Sail2_instr_kinds.v | |
| parent | eae01f8c348235ea552c67ce323a1ada3dbc8b08 (diff) | |
Coq: fix up some barrier/memory definitions for RISC-V
Diffstat (limited to 'lib/coq/Sail2_instr_kinds.v')
| -rw-r--r-- | lib/coq/Sail2_instr_kinds.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v index c93e9e93..eadc567a 100644 --- a/lib/coq/Sail2_instr_kinds.v +++ b/lib/coq/Sail2_instr_kinds.v @@ -144,7 +144,7 @@ Inductive barrier_kind := (* AArch64 barriers *) | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB - | Barrier_TM_COMMIT + (* | Barrier_TM_COMMIT*) (* MIPS barriers *) | Barrier_MIPS_SYNC (* RISC-V barriers *) @@ -204,11 +204,11 @@ Inductive instruction_kind := | IK_mem_read : read_kind -> instruction_kind | IK_mem_write : write_kind -> instruction_kind | IK_mem_rmw : (read_kind * write_kind) -> instruction_kind - | IK_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address), + | IK_branch : unit -> instruction_kind (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address), indirect/computed-branch (single nia of kind NIA_indirect_address) and branch/jump (single nia of kind NIA_concrete_address) *) | IK_trans : trans_kind -> instruction_kind - | IK_simple : instruction_kind. + | IK_simple : unit -> instruction_kind. (* instance (Show instruction_kind) |