From 51cfd8e43bc095e567f22b1768eb2743be8ffc22 Mon Sep 17 00:00:00 2001
From: Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>
Date: Tue, 18 Aug 2020 19:53:51 +0200
Subject: 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
---
 aarch64/Asm.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'aarch64/Asm.v')

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
-- 
cgit