diff options
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index cf8c51a2..a648b437 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -156,6 +156,10 @@ val build_context : specification -> memory_reads -> memory_writes -> memory_wri val initial_instruction_state : context -> string -> list register_value -> instruction_state (* string is a function name, list of value are the parameters to that function *) +type instruction_or_decode_error = + | IDE_instr of instruction * Interp.value + | IDE_decode_error of decode_error + (** propose to remove the following type and use the above instead *) type i_state_or_error = | Instr of instruction * instruction_state @@ -198,4 +202,4 @@ val instruction_analysis : -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind) -val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state string unit +val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state unit |