aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Splitting.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-04-02 16:25:25 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-04-02 16:25:25 +0200
commit170284b51766112e29d6bbfe519bad9f6da95269 (patch)
tree13a163ccee48cee0512a8af484b394623cdce030 /backend/Splitting.ml
parent2e30ad9698a6f24a8a746f68b30c235913006392 (diff)
parent959432fa13a899290db5236f93575a8bfdc13bb5 (diff)
downloadcompcert-170284b51766112e29d6bbfe519bad9f6da95269.tar.gz
compcert-170284b51766112e29d6bbfe519bad9f6da95269.zip
Merge branch 'master' into dwarf
Diffstat (limited to 'backend/Splitting.ml')
-rw-r--r--backend/Splitting.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/Splitting.ml b/backend/Splitting.ml
index 3530ba99..53600c98 100644
--- a/backend/Splitting.ml
+++ b/backend/Splitting.ml
@@ -163,6 +163,8 @@ let ren_instr f maps pc i =
Itailcall(sg, ren_ros before ros, ren_regs before args)
| Ibuiltin(ef, args, res, s) ->
Ibuiltin(ef, ren_regs before args, ren_reg after res, s)
+ | Iannot(ef, args, s) ->
+ Iannot(ef, List.map (AST.map_annot_arg (ren_reg before)) args, s)
| Icond(cond, args, s1, s2) ->
Icond(cond, ren_regs before args, s1, s2)
| Ijumptable(arg, tbl) ->