diff options
Diffstat (limited to 'backend/Stacking.v')
| -rw-r--r-- | backend/Stacking.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/backend/Stacking.v b/backend/Stacking.v index 1f0c4542..85ac9335 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -186,6 +186,8 @@ Definition transl_instr Mstore chunk (transl_addr fe addr) args src :: k | Lcall sig ros => Mcall sig ros :: k + | Lalloc => + Malloc :: k | Llabel lbl => Mlabel lbl :: k | Lgoto lbl => @@ -222,5 +224,8 @@ Definition transf_function (f: Linear.function) : option Mach.function := f.(Linear.fn_stacksize) fe.(fe_size)). +Definition transf_fundef (f: Linear.fundef) : option Mach.fundef := + AST.transf_partial_fundef transf_function f. + Definition transf_program (p: Linear.program) : option Mach.program := - transform_partial_program transf_function p. + transform_partial_program transf_fundef p. |