diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-08-18 19:53:51 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-08-18 19:53:51 +0200 |
| commit | 51cfd8e43bc095e567f22b1768eb2743be8ffc22 (patch) | |
| tree | 93dbcaca1b8dd38930d650924b9a94462beaf8e7 /aarch64/Asm.v | |
| parent | 7b68243df6cc0529e7d666e3c7f2c7f09c6af1a7 (diff) | |
| download | compcert-kvx-51cfd8e43bc095e567f22b1768eb2743be8ffc22.tar.gz compcert-kvx-51cfd8e43bc095e567f22b1768eb2743be8ffc22.zip | |
Prove exec_body_dont_move_PC
Modify Asmblock.preg to combine iregsp and freg into dreg (dreg might be
a misnomer since not all iregs are data regs)
TODO: Adjust names of PArithP, PArithPP and the like
Diffstat (limited to 'aarch64/Asm.v')
| -rw-r--r-- | aarch64/Asm.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index dc1faddd..4de1a9d0 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -836,10 +836,10 @@ Qed. Definition data_preg (r: preg) : bool := match r with - | IR X16 => false - | IR X30 => false - | IR _ => true - | FR _ => true + | DR (IR' X16) => false + | DR (IR' X30) => false + | DR (IR' _) => true + | DR (FR' _) => true | CR _ => false (* | SP => true; subsumed by IR (iregsp) *) | PC => false |