diff options
| author | Kathy Gray | 2015-07-01 11:02:01 +0100 |
|---|---|---|
| committer | Kathy Gray | 2015-07-01 11:02:01 +0100 |
| commit | 1e063c15e4895dddac394511c94bc8b1f634fa5c (patch) | |
| tree | 359f07c06cead2a5d971d6284049dff422d31e20 | |
| parent | 67aabe1c9d7633fe89640482225aaa93f4c0704d (diff) | |
Go on despite the presence of an exit in exhaustive mode
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 7 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 5 |
2 files changed, 7 insertions, 5 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 882522d7..ba762162 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -525,7 +525,7 @@ let rec interp_to_outcome mode context thunk = | Interp.Exit e -> Escape (match e with | E_aux (E_lit (L_aux L_unit _)) _ -> Nothing - | _ -> Just (IState (Interp.set_in_context next_state e) context) end) + | _ -> Just (IState (Interp.set_in_context next_state e) context) end) (IState next_state context) end end @@ -576,8 +576,9 @@ let rec ie_loop mode register_values (IState interp_state context) = match interp mode (IState interp_state context) with | Done -> [] | Error msg -> [E_error msg] - | Escape Nothing -> [E_escape] - | Escape _ -> [E_escape] (*Do we want to record anything about the escape expression, which may be a function call*) + | Escape Nothing i_state -> E_escape :: (ie_loop mode register_values i_state) + (*Do we want to record anything about the escape expression, which may be a function call*) + | Escape _ i_state -> E_escape :: (ie_loop mode register_values i_state) | Read_reg reg i_state_fun -> let v = match register_values with | Nothing -> unknown_reg (reg_size reg) 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 |