diff options
| author | Christopher Pulte | 2016-09-21 10:42:09 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-09-21 10:42:09 +0100 |
| commit | b73a7daa6d2b661659ecf066d25d146cadaec1e8 (patch) | |
| tree | 47748211890234c43e13eec2611c97ed68d9e45d /src/lem_interp | |
| parent | ea2d92c84d879719f44b3f4bf3c9dfabd8d8ea29 (diff) | |
fixes
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 8b81b83f..9a06b0ba 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -516,7 +516,6 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Barrier_DSB_ST" -> DSB_ST | "Barrier_DSB_LD" -> DSB_LD | "Barrier_ISB" -> ISB - | "Barrier_Sync" -> Sync end) | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ (Interp.V_ctor (Id_aux (Id r) _) _ _ _) -> |