diff options
| author | Shaked Flur | 2017-05-28 11:30:15 +0100 |
|---|---|---|
| committer | Shaked Flur | 2017-05-28 11:30:15 +0100 |
| commit | 8887fcb1357bf40b97ec986be55e42649e38aaee (patch) | |
| tree | b681b2d9e574180e07686a038466939b52f7ad03 /src | |
| parent | e54244cfe43bbf8fa34c09132eccba597e2bce45 (diff) | |
fixed exmem
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 4 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 23e2160b..9c88eec7 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -360,7 +360,7 @@ type action = | Write_mem of id * value * maybe (nat * nat) * value | Write_ea of id * value | Write_memv of id * value * value - | Excl_res of id * value + | Excl_res of id | Write_memv_tagged of id * value * value * value | Barrier of id * value | Footprint of id * value @@ -2248,7 +2248,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = else if has_eamem_effect effects then mk_thunk_frame (Write_ea (id_of_string name_ext) v) else if has_exmem_effect effects - then mk_thunk_frame (Excl_res (id_of_string name_ext) v) + then mk_hole_frame (Excl_res (id_of_string name_ext)) else if has_wmv_effect effects then let (wv,v) = match v with diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 280b1097..f0d7dec4 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -433,7 +433,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev (Ivh_error (Interp_interface.Internal_error ("Write memory request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_ea _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Write ea request in a " ^ errk_str)), events_out) - | (Interp.Action (Interp.Excl_res _ _) _,_,_) -> + | (Interp.Action (Interp.Excl_res _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Exclusive result request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_memv _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out) @@ -831,7 +831,7 @@ let rec interp_to_outcome mode context thunk = Write_ea write_k (Address_lifted location address_int) length tracking (IState next_state context) else Error "Memory address for write is not 64 bits" | _ -> Error ("Memory function " ^ i ^ " to signal impending write, not found") end, lm) - | Interp.Excl_res (Id_aux (Id i) _) loc_val -> + | Interp.Excl_res (Id_aux (Id i) _) -> (match excl_res with | (Just (i', ER return)) -> Excl_res (fun b -> |