diff options
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 1eb16d9d..caf6f52b 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -75,7 +75,9 @@ let rec interp_to_outcome mode thunk = match List.lookup i memory_functions with | (Just (_,Just write_k,f)) -> Write_mem write_k (f loc_val) (extern_value true write_val) (fun b -> next_state) | _ -> Error ("Memory " ^ i ^ " function with write kind not found") - end + end + | Interp.Barrier (Id_aux (Id i) _) lval -> + Barrier Interp.Barrier_plain next_state (* TODO set up some barrier functions and see if the value would be anything needed *) | Interp.Call_extern i value -> match List.lookup i external_functions with | Nothing -> Error ("External function not available " ^ i) |