diff options
| author | Robert Norton | 2016-11-30 15:42:12 +0000 |
|---|---|---|
| committer | Robert Norton | 2016-11-30 15:42:12 +0000 |
| commit | 67cb941a3e56730a631bf740c9d41dd5e6c1dc07 (patch) | |
| tree | 0e0b9fb9092bd97986897a9a9d2dafc3756cebff /src/gen_lib/deep_shallow_convert.lem | |
| parent | 45bd517a0c7a7b0a2d51bc9bae575218bfe54534 (diff) | |
add new barrier kind for MIPS (only one for now).
Diffstat (limited to 'src/gen_lib/deep_shallow_convert.lem')
| -rw-r--r-- | src/gen_lib/deep_shallow_convert.lem | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem index aa16f069..23c34222 100644 --- a/src/gen_lib/deep_shallow_convert.lem +++ b/src/gen_lib/deep_shallow_convert.lem @@ -455,6 +455,7 @@ let barrier_kindToInterpValue = function | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ()) | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ()) | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ()) + | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ()) end let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync @@ -468,6 +469,7 @@ let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB + | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC | V_tuple [v] -> barrier_kindFromInterpValue v | v -> failwith ("fromInterpValue barrier_kind: unexpected value. " ^ Interp.debug_print_value v) |