From 9256ae56302cd90e57181bb187db816bea9523e6 Mon Sep 17 00:00:00 2001 From: Gaga Date: Fri, 23 Aug 2024 23:58:25 -0400 Subject: [PATCH] Mgetparent -> Mgetparam --- backend/Stacking.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backend/Stacking.v b/backend/Stacking.v index 1377a666aa..34e1558be5 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -130,7 +130,7 @@ Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg m (** Translation of a Linear instruction. Prepends the corresponding Mach instructions to the given list of instructions. [Lgetstack] and [Lsetstack] moves between registers and stack slots - are turned into [Mgetstack], [Mgetparent] or [Msetstack] instructions + are turned into [Mgetstack], [Mgetparam] or [Msetstack] instructions at offsets determined by the frame environment. Instructions and addressing modes are modified as described previously. Code to restore the values of callee-save registers is inserted