summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp.lem2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index cbbbc091..ea06fa5d 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -120,7 +120,7 @@ let eenv = LEnv 1 []
type read_kind = Read_plain | Read_reserve | Read_acquire
type write_kind = Write_plain | Write_conditional | Write_release
-type barrier_kind = Plain | Sync | LwSync | Eieio | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD
+type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (* PS removed "plain" and added "Isync" and "ISB" *)
(*top_level is a tuple of
(all definitions, letbound and enum values, register values, Typedef union constructors, sub register mappings, and register aliases) *)