From 3a4358d34cca39d61da4a21953be2a55f0a0a89e Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 15 Sep 2017 18:26:16 +0100
Subject: x86: implement regfp analysis function (no control flow yet)

---
 src/lem_interp/interp_inter_imp.lem | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src')

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) _) _ _ _) ->
-- 
cgit v1.2.3