aboutsummaryrefslogtreecommitdiffstats
path: root/backend/IRC.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-11-18 21:07:29 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-11-18 21:07:29 +0100
commit8384d27c122ec4ca4b7ad0f524df52b61a49c66a (patch)
treed86ff8780c4435d3b4fe92b5251e0f9b447b86c7 /backend/IRC.ml
parent362bdda28ca3c4dcc992575cbbe9400b64425990 (diff)
parente6e036b3f285d2f3ba2a5036a413eb9c7d7534cd (diff)
downloadcompcert-kvx-8384d27c122ec4ca4b7ad0f524df52b61a49c66a.tar.gz
compcert-kvx-8384d27c122ec4ca4b7ad0f524df52b61a49c66a.zip
Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8
Diffstat (limited to 'backend/IRC.ml')
-rw-r--r--backend/IRC.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/backend/IRC.ml b/backend/IRC.ml
index 785b0a2d..29d224c8 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -102,7 +102,7 @@ after IRC elimination, when assigning a stack slot to a spilled variable. *)
let name_of_loc = function
| R r ->
- begin match Machregsaux.name_of_register r with
+ begin match Machregsnames.name_of_register r with
| None -> "fixed-reg"
| Some s -> s
end
@@ -247,12 +247,10 @@ let class_of_loc = function
let no_spill_class = 2
-let reserved_registers = ref ([]: mreg list)
-
let rec remove_reserved = function
| [] -> []
| hd :: tl ->
- if List.mem hd !reserved_registers
+ if List.mem hd !CPragmas.reserved_registers
then remove_reserved tl
else hd :: remove_reserved tl