diff options
Diffstat (limited to 'aarch64/Asm.v')
| -rw-r--r-- | aarch64/Asm.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 0959d9ca..369e6f3b 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -841,6 +841,6 @@ Definition data_preg (r: preg) : bool := | IR _ => true | FR _ => true | CR _ => false - | SP => true + (* | SP => true; subsumed by IR (iregsp) *) | PC => false end. |