Merged in ojno/sail (pull request #1)

Footprint exhaustive evaluation fixes

Approved-by: Jonathan French <me@jonathanfrench.net>

1 files changed, 7 insertions, 7 deletions

diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index d6f6e30c..6978aeb9 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -292,7 +292,7 @@ let run
         interact mode env stack
       | "e" | "exh" | "exhaust" ->
         interactf "interpreting exhaustively from current state\n";
-        let events = interp_exhaustive None stack in
+        let events = interp_exhaustive false None stack in
         interactf "%s" (format_events events);
         interact mode env stack
       | "c" | "cont" | "continuation" ->
@@ -339,7 +339,7 @@ let run
         let (top_exp,(top_env,top_mem)) = top_frame_exp_state stack in
         let loc = get_loc (compact_exp top_exp) in
         if mode = Step || force then begin
-          interactf "%s\n" (Pretty_interp.pp_exp top_env Printing_functions.red true top_exp);
+          interactf "%s\n" (Pretty_interp.pp_exp top_env top_mem Printing_functions.red true top_exp);
           interact mode env' state
         end else
           mode in
@@ -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) next))
+              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) 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) next))
+              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next))
               choose_order (false,mode,!track_dependencies,env'); in
             (step i_state,env',i_state) end
         | Escape0(Some e,_) ->
@@ -462,15 +462,15 @@ let run
         | Write_memv1 _ -> assert false)
         (*| _ -> assert false*)
       in
-      loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies) next) in
+      loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies false) 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 in
+  let imode = make_mode eager_eval !track_dependencies false 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") 
-    (Pretty_interp.pp_exp top_env Printing_functions.red true top_exp);
+    (Pretty_interp.pp_exp top_env top_mem Printing_functions.red true top_exp);
   try
     Printexc.record_backtrace true;
     loop mode (reg, mem,tagmem) (Interp_inter_imp.interp0 imode istate)