Il suffit d'ajouter un temporaire spécial (utilisé nulle part ailleurs) m et de considérer la lecture en mémoire comme la lecture de m et l'écriture en mémoire comme l'écriture de m. On écrira alors les lignes

| Mem e -> m :: lus_par_exp e

et

| Move_mem (t, e) -> [ m ]

à la place des lignes correspondantes dans lus_par_exp et écrits_par_stm.