summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Machregs.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index d057dce..baad496 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -105,6 +105,8 @@ Module IndexedMreg <: INDEXED_TYPE.
Qed.
End IndexedMreg.
+Definition is_stack_reg (r: mreg) : bool := false.
+
(** ** Destroyed registers, preferred registers *)
Definition destroyed_by_op (op: operation): list mreg :=