diff options
| author | Alasdair Armstrong | 2017-11-29 19:29:48 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-29 19:29:48 +0000 |
| commit | 16c475fff5b1942eacc4f399ff14a0bca0c9cec2 (patch) | |
| tree | 78931fdee36cbb9cde2001853aa016cf8cc67110 /src/lem_interp | |
| parent | 636d81ee6afba69b7a2516e8149eeef3691cd67e (diff) | |
Better lem_ast tagging and interpreter tweaks
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 3 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 8 |
2 files changed, 6 insertions, 5 deletions
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") |
