diff options
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index d35653c9..a39f3f3a 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -535,6 +535,7 @@ 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 end) | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ (Interp.V_ctor (Id_aux (Id r) _) _ _ _) -> |