diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 16 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 7 |
2 files changed, 8 insertions, 15 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index cb5868ea..76dc01a1 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -506,18 +506,18 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Just addr -> addr | Nothing -> failwith "get_nia encountered invalid address" end in let dia_to_dia = function - | Interp.V_ctor (Id_aux (Id "DIA_none") _) _ _ _ -> DIA_none - | Interp.V_ctor (Id_aux (Id "DIA_concrete") _) _ _ address -> + | Interp.V_ctor (Id_aux (Id "DIAFP_none") _) _ _ _ -> DIA_none + | Interp.V_ctor (Id_aux (Id "DIAFP_concrete") _) _ _ address -> DIA_concrete_address (get_addr address) - | Interp.V_ctor (Id_aux (Id "DIA_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) + | Interp.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) | _ -> failwith "Register footprint analysis did not return dia of expected type" end in let nia_to_nia = function - | Interp.V_ctor (Id_aux (Id "NIA_successor") _) _ _ _-> NIA_successor - | Interp.V_ctor (Id_aux (Id "NIA_concrete_address") _) _ _ address -> + | Interp.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor + | Interp.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address -> NIA_concrete_address (get_addr address) - | Interp.V_ctor (Id_aux (Id "NIA_LR") _) _ _ _ -> NIA_LR - | Interp.V_ctor (Id_aux (Id "NIA_CTR") _) _ _ _ -> NIA_CTR - | Interp.V_ctor (Id_aux (Id "NIA_register") _) _ _ reg -> + | Interp.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR + | Interp.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR + | Interp.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg -> NIA_register (reg_to_reg_name reg) | _ -> failwith "Register footprint analysis did not return nia of expected type" end in let ik_to_ik = function diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 86778bee..63040ebf 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -1399,10 +1399,3 @@ instance (Eq decode_error) let (=) = decode_error_equal let (<>) = decode_error_inequal end - -type regfp = - | RFull of (string) - | RSlice of (string * integer * integer) - | RSliceBit of (string * integer) - | RField of (string * string) - |