diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-08-22 09:46:37 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-08-22 09:46:37 +0200 |
| commit | 33dfbe7601ad16fcea5377563fa7ceb4053cb85a (patch) | |
| tree | 962468d4f01ae9620441a97082c826bc6fdf8c5a /backend/Allocation.v | |
| parent | 4f187fdafdac0cf4a8b83964c89d79741dbd813e (diff) | |
| download | compcert-kvx-33dfbe7601ad16fcea5377563fa7ceb4053cb85a.tar.gz compcert-kvx-33dfbe7601ad16fcea5377563fa7ceb4053cb85a.zip | |
Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.
Use EF_debug instead of EF_annot for line number annotations.
Introduce PrintAsmaux.print_debug_info (very incomplete).
powerpc/Asmexpand: revise expand_memcpy_small.
Diffstat (limited to 'backend/Allocation.v')
| -rw-r--r-- | backend/Allocation.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 5499c1c5..196a4075 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -697,7 +697,7 @@ Fixpoint add_equations_builtin_arg match arg, arg' with | BA r, BA l => Some (add_equation (Eq Full r l) e) - | BA r, BA_longofwords (BA lhi) (BA llo) => + | BA r, BA_splitlong (BA lhi) (BA llo) => assertion (typ_eq (env r) Tlong); Some (add_equation (Eq Low r llo) (add_equation (Eq High r lhi) e)) | BA_int n, BA_int n' => @@ -724,7 +724,7 @@ Fixpoint add_equations_builtin_arg assertion (ident_eq id id'); assertion (Int.eq_dec ofs ofs'); Some e - | BA_longofwords hi lo, BA_longofwords hi' lo' => + | BA_splitlong hi lo, BA_splitlong hi' lo' => do e1 <- add_equations_builtin_arg env hi hi' e; add_equations_builtin_arg env lo lo' e1 | _, _ => @@ -763,7 +763,7 @@ Definition remove_equations_builtin_res (env: regenv) (res: builtin_res reg) (res': builtin_res mreg) (e: eqs) : option eqs := match res, res' with | BR r, BR r' => Some (remove_equation (Eq Full r (R r')) e) - | BR r, BR_longofwords (BR rhi) (BR rlo) => + | BR r, BR_splitlong (BR rhi) (BR rlo) => assertion (typ_eq (env r) Tlong); if mreg_eq rhi rlo then None else Some (remove_equation (Eq Low r (R rlo)) |