diff options
Diffstat (limited to 'src/lem_interp/interp_utilities.lem')
| -rw-r--r-- | src/lem_interp/interp_utilities.lem | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem index e80a2323..b808208b 100644 --- a/src/lem_interp/interp_utilities.lem +++ b/src/lem_interp/interp_utilities.lem @@ -66,12 +66,14 @@ let rec has_effect which efcts = | [] -> false | (BE_aux e _)::efcts -> match (which,e) with - | (BE_rreg,BE_rreg) -> true - | (BE_wreg,BE_wreg) -> true - | (BE_rmem,BE_rmem) -> true - | (BE_wmem,BE_wmem) -> true - | (BE_barr,BE_barr) -> true - | (BE_undef,BE_undef) -> true + | (BE_rreg,BE_rreg) -> true + | (BE_wreg,BE_wreg) -> true + | (BE_rmem,BE_rmem) -> true + | (BE_wmem,BE_wmem) -> true + | (BE_wmv,BE_wmv) -> true + | (BE_eamem,BE_eamem) -> true + | (BE_barr,BE_barr) -> true + | (BE_undef,BE_undef) -> true | (BE_unspec,BE_unspec) -> true | (BE_nondet,BE_nondet) -> true | (BE_depend,BE_depend) -> true @@ -81,6 +83,8 @@ let rec has_effect which efcts = let has_rmem_effect = has_effect BE_rmem let has_barr_effect = has_effect BE_barr let has_wmem_effect = has_effect BE_wmem +let has_eamem_effect = has_effect BE_eamem +let has_wmv_effect = has_effect BE_wmv let has_depend_effect = has_effect BE_depend let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t |