diff options
Diffstat (limited to 'backend/Stacking.v')
| -rw-r--r-- | backend/Stacking.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/Stacking.v b/backend/Stacking.v index f51848f2..7b382d05 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -97,6 +97,8 @@ Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg m | BA_addrglobal id ofs => BA_addrglobal id ofs | BA_splitlong hi lo => BA_splitlong (transl_builtin_arg fe hi) (transl_builtin_arg fe lo) + | BA_addptr a1 a2 => + BA_addptr (transl_builtin_arg fe a1) (transl_builtin_arg fe a2) end. (** Translation of a Linear instruction. Prepends the corresponding |