summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorKathy Gray2014-10-04 17:39:54 +0100
committerKathy Gray2014-10-04 17:39:54 +0100
commit072f8a43eb471d8e0425370aabc25fbb8d6a2511 (patch)
tree4ee06831a11c8734db11463a344430e3419bedda /src
parentf2b2b02654caf2e11ccef6cb459ecd27611c23a4 (diff)
clarify Step constructor
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/run_interp.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 37c73d66..a9c22b6c 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -291,7 +291,7 @@ let rec perform_action ((reg, mem) as env) = function
perform_action env (Write_mem (id, n, slice, V_vector(zero_big_int, true, [value])))
(* extern functions *)
| Call_extern (name, arg) -> eval_external name arg, env
- | Step _ | Nondet _ | Exit _ -> unit_lit, env
+ | Interp.Step _ | Nondet _ | Exit _ -> unit_lit, env
| _ -> assert false
;;
@@ -406,7 +406,7 @@ let run
| Call_extern (f, arg) ->
show "call_lib" (sprintf "%s(%s)" f (val_to_string_internal arg)) right (val_to_string_internal return);
step (),env',s
- | Step _ ->
+ | Interp.Step _ ->
assert (return = unit_lit);
show "breakpoint" "" "" "";
step ~force:true (),env',s