diff options
| author | Robert Norton | 2017-05-11 14:54:32 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-05-24 10:56:59 +0100 |
| commit | e9b40edcc325bfe5a0e3566c61ee12a236c5ddf8 (patch) | |
| tree | f81ad5395520cc66a38d08d8ca1965f4e2bc30a3 /src/pretty_print_lem.ml | |
| parent | a6c4b61f4ae06845663eb06b2a0efc98a42ccac3 (diff) | |
Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index b55685f4..92735f87 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -125,7 +125,7 @@ let effectful (Effect_aux (eff,_)) = List.exists (fun (BE_aux (eff,_)) -> match eff with - | BE_rreg | BE_wreg | BE_rmem | BE_wmem | BE_eamem | BE_wmv + | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet | BE_escape -> true | _ -> false) effs |