diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 411ad3fc..6ee13d60 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -587,7 +587,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Barrier_DSB_ST" -> Barrier_DSB_ST | "Barrier_DSB_LD" -> Barrier_DSB_LD | "Barrier_ISB" -> Barrier_ISB - | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC + | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC + | "Barrier_x86_MFENCE" -> Barrier_x86_MFENCE end) | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) -> |