diff options
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 8db772c8..bc3f7d7b 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -459,8 +459,9 @@ type outcome = | Nondet_choice of list instruction_state * instruction_state (* Stop for incremental stepping, function can be used to display function call data *) | Internal of maybe string * maybe (unit -> string) * instruction_state -(* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler *) -| Escape of maybe instruction_state +(* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler + The non-optional instruction_state is what we would be doing if we're not escaping. This is for exhaustive interp*) +| Escape of maybe instruction_state * instruction_state | Done | Error of string |