diff options
Diffstat (limited to 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index c8f8ea82..f54c8698 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -178,6 +178,10 @@ let rec print_annot print_preg sp_reg_name oc = function fprintf oc "(%a * 0x100000000 + %a)" (print_annot print_preg sp_reg_name) hi (print_annot print_preg sp_reg_name) lo + | BA_addptr(a1, a2) -> + fprintf oc "(%a + %a)" + (print_annot print_preg sp_reg_name) a1 + (print_annot print_preg sp_reg_name) a2 let print_annot_text print_preg sp_reg_name oc txt args = let print_fragment = function |