From 16c475fff5b1942eacc4f399ff14a0bca0c9cec2 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 29 Nov 2017 19:29:48 +0000
Subject: Better lem_ast tagging and interpreter tweaks

---
 src/lem_interp/interp_inter_imp.lem | 3 ++-
 src/lem_interp/run_interp_model.ml  | 8 ++++----
 2 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'src/lem_interp')

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 68f82ccb..e9533a2a 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -440,7 +440,8 @@ let rec interp_to_value_helper debug arg ivh_mode err_str instr direction regist
       (Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
     | (Interp.Action (Interp.Write_memv_tagged _ _ _ _) _,_,_) ->
       (Ivh_error (Interp_interface.Internal_error ("Write memory value tagged request in a " ^ errk_str)), events_out)
-    | _ -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str)), events_out)
+    | (outcome, _, _) ->
+       (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str ^ " " ^ Interp.string_of_outcome outcome)), events_out)
 end
 
 let call_external_functions direction outcome = 
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 6978aeb9..81f0a5fd 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -433,7 +433,7 @@ let run
               (List.combine nondets (List.map (fun _ -> Random.bits ()) nondets)) in
           show "nondeterministic evaluation begun" "" "" "";
           let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') -> 
-              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next))
+              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies true) next))
               choose_order (false,mode,!track_dependencies,env'); in
           show "nondeterministic evaluation ended" "" "" "";
           (step next,env',next)
@@ -445,7 +445,7 @@ let run
           else begin
             show "undefined triggered a non_det" "" "" "";
             let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') -> 
-              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next))
+              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies true) next))
               choose_order (false,mode,!track_dependencies,env'); in
             (step i_state,env',i_state) end
         | Escape0(Some e,_) ->
@@ -462,11 +462,11 @@ let run
         | Write_memv1 _ -> assert false)
         (*| _ -> assert false*)
       in
-      loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies false) next) in
+      loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies true) next) in
   let mode = match mode with
   | None -> if eager_eval then Run else Step
   | Some m -> m in
-  let imode = make_mode eager_eval !track_dependencies false in
+  let imode = make_mode eager_eval !track_dependencies true in
   let (IState(instr_state,context)) = istate in
   let (top_exp,(top_env,top_mem)) = top_frame_exp_state instr_state in
   interactf "%s: %s %s\n" (grey name) (blue "evaluate") 
-- 
cgit v1.2.3