summaryrefslogtreecommitdiff
path: root/backend/Mach.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Mach.v')
-rw-r--r--backend/Mach.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Mach.v b/backend/Mach.v
index 316e788..f0fb56a 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -273,7 +273,7 @@ Inductive state: Type :=
Definition parent_sp (s: list stackframe) : val :=
match s with
- | nil => Vptr Mem.nullptr Int.zero
+ | nil => Vzero
| Stackframe f sp ra c :: s' => sp
end.