aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Locations.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-08-22 09:46:37 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-08-22 09:46:37 +0200
commit33dfbe7601ad16fcea5377563fa7ceb4053cb85a (patch)
tree962468d4f01ae9620441a97082c826bc6fdf8c5a /backend/Locations.v
parent4f187fdafdac0cf4a8b83964c89d79741dbd813e (diff)
downloadcompcert-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/Locations.v')
-rw-r--r--backend/Locations.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Locations.v b/backend/Locations.v
index 4ec24a14..439cd2dc 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -381,7 +381,7 @@ Module Locmap.
match res with
| BR r => set (R r) v m
| BR_none => m
- | BR_longofwords hi lo =>
+ | BR_splitlong hi lo =>
setres lo (Val.loword v) (setres hi (Val.hiword v) m)
end.