Currently, the tool treats expressions of the form domain(E) and range(E) as equivalent to E. We should add proper support for these functions, or at the very least make sure that it is sound to treat them as equivalent to the identity.
Note that domain is used to define ``, which in turn are used to define IC-after and `TLBI-after`.
let C_TLBI = TLBI & domain(po; [dsb.full])
let C_IC = IC & domain(po; [dsb.full])
Currently, the tool treats expressions of the form
domain(E)andrange(E)as equivalent toE. We should add proper support for these functions, or at the very least make sure that it is sound to treat them as equivalent to the identity.Note that
domainis used to define ``, which in turn are used to defineIC-afterand `TLBI-after`.