diff options
| author | Peter Sewell | 2017-03-24 13:39:24 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-03-24 13:39:24 +0000 |
| commit | 888d06d3e224b9063f330aec22a4e23a9c89a48a (patch) | |
| tree | 47cfe08fa33f5d238d806ba44304657b96ccc545 | |
| parent | 4f31d4d7f0e1c5d77d65fee14f4fb8e149201e73 (diff) | |
Christopher, Peter: make "run_interp_model.ml" build again (endianness)
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index af9a1e0e..8be5354a 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -397,7 +397,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 !default_endian) next)) + loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies) next)) choose_order (false,mode,!track_dependencies,env'); in show "nondeterministic evaluation ended" "" "" ""; (step next,env',next) @@ -409,7 +409,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 !default_endian) next)) + loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies) next)) choose_order (false,mode,!track_dependencies,env'); in (step i_state,env',i_state) end | Escape0(Some e,_) -> @@ -426,11 +426,11 @@ let run | Write_memv1 _ -> assert false) (*| _ -> assert false*) in - loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies !default_endian) next) in + loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies) 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 !default_endian in + let imode = make_mode eager_eval !track_dependencies 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") |