1 files changed, 3 insertions, 4 deletions
diff --git a/backend/Mach.v b/backend/Mach.v
index f727504..c64903b 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -70,7 +70,9 @@ Record function: Set := mkfunction
   { fn_sig: signature;
     fn_code: code;
     fn_stacksize: Z;
-    fn_framesize: Z }.
+    fn_framesize: Z;
+    fn_link_ofs: int;
+    fn_retaddr_ofs: int }.
 
 Definition fundef := AST.fundef function.
 
@@ -137,6 +139,3 @@ Definition find_function_ptr
       Genv.find_symbol ge symb
   end.
 
-Definition align_16_top (lo hi: Z) :=
-  Zmax 0 (((hi - lo + 15) / 16) * 16 + lo).
-