diff options
| author | Robert Norton | 2017-09-15 18:26:16 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-09-15 18:26:49 +0100 |
| commit | 3a4358d34cca39d61da4a21953be2a55f0a0a89e (patch) | |
| tree | 37e44c046f80e9918e83732a8b9e588e62353b73 /src | |
| parent | a97cd6081df6a76c9daa34c773d82f21f5d014c8 (diff) | |
x86: implement regfp analysis function (no control flow yet)
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) _) _ _ _) -> |