aboutsummaryrefslogtreecommitdiffstats
path: root/backend/RTLgen.v
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-21 19:13:07 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-21 19:13:07 +0200
commit4b9b0e8f988cdfa1f848919b41bfe24c6e9a052a (patch)
tree0068ca2f3c45ffb7e07db62d681ccd3b96bcb167 /backend/RTLgen.v
parenta34b64ee2e7a535ebc0fc731243ab520c4ba430f (diff)
parent9147350fdb47f3471ce6d9202b7c996f79ffab2d (diff)
downloadcompcert-4b9b0e8f988cdfa1f848919b41bfe24c6e9a052a.tar.gz
compcert-4b9b0e8f988cdfa1f848919b41bfe24c6e9a052a.zip
Merge branch 'debugscopes' into debug_locations
Conflicts: debug/CtoDwarf.ml debug/DwarfPrinter.ml
Diffstat (limited to 'backend/RTLgen.v')
-rw-r--r--backend/RTLgen.v13
1 files changed, 7 insertions, 6 deletions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index d818de58..3da961c6 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -415,11 +415,12 @@ Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list
a1' :: convert_builtin_args al rl1
end.
-Definition convert_builtin_res (map: mapping) (r: builtin_res ident) : mon (builtin_res reg) :=
- match r with
- | BR id => do r <- find_var map id; ret (BR r)
- | BR_none => ret BR_none
- | _ => error (Errors.msg "RTLgen: bad builtin_res")
+Definition convert_builtin_res (map: mapping) (oty: option typ) (r: builtin_res ident) : mon (builtin_res reg) :=
+ match r, oty with
+ | BR id, _ => do r <- find_var map id; ret (BR r)
+ | BR_none, None => ret BR_none
+ | BR_none, Some _ => do r <- new_reg; ret (BR r)
+ | _, _ => error (Errors.msg "RTLgen: bad builtin_res")
end.
(** Translation of an expression. [transl_expr map a rd nd]
@@ -598,7 +599,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
let al := exprlist_of_expr_list (params_of_builtin_args args) in
do rargs <- alloc_regs map al;
let args' := convert_builtin_args args rargs in
- do res' <- convert_builtin_res map res;
+ do res' <- convert_builtin_res map (sig_res (ef_sig ef)) res;
do n1 <- add_instr (Ibuiltin ef args' res' nd);
transl_exprlist map al rargs n1
| Sseq s1 s2 =>