6 files changed, 32 insertions, 15 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 =>
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 559ab3a2..19f6f1f4 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -234,6 +234,7 @@ Proof.
   intros. inv H1; simpl.
 - eapply match_env_update_var; eauto.
 - auto.
+- eapply match_env_update_temp; eauto.
 Qed.
 
 (** Matching and [let]-bound variables. *)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 41b5016f..1e665002 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -814,7 +814,10 @@ Inductive tr_builtin_res: mapping -> builtin_res ident -> builtin_res reg -> Pro
       map.(map_vars)!id = Some r ->
       tr_builtin_res map (BR id) (BR r)
   | tr_builtin_res_none: forall map,
-      tr_builtin_res map BR_none BR_none.
+      tr_builtin_res map BR_none BR_none
+  | tr_builtin_res_fresh: forall map r,
+      ~reg_in_map map r ->
+      tr_builtin_res map BR_none (BR r).
 
 (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c],
   starting at node [ns], contains instructions that perform the Cminor
@@ -1214,14 +1217,17 @@ Proof.
 Qed.
 
 Lemma convert_builtin_res_charact:
-  forall map res s res' s' INCR
-    (TR: convert_builtin_res map res s = OK res' s' INCR)
+  forall map oty res s res' s' INCR
+    (TR: convert_builtin_res map oty res s = OK res' s' INCR)
     (WF: map_valid map s),
   tr_builtin_res map res res'.
 Proof.
-  destruct res; simpl; intros; monadInv TR. 
-- constructor.  unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto.
-- constructor.
+  destruct res; simpl; intros.
+- monadInv TR. constructor.  unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto.
+- destruct oty; monadInv TR.
++ constructor. eauto with rtlg. 
++ constructor.
+- monadInv TR.
 Qed.
 
 Lemma transl_stmt_charact:
diff --git a/test/regression/builtins-arm.c b/test/regression/builtins-arm.c
index 91a8e890..643c8f1a 100644
--- a/test/regression/builtins-arm.c
+++ b/test/regression/builtins-arm.c
@@ -23,7 +23,10 @@ int main(int argc, char ** argv)
   y = 0;
   __builtin_write32_reversed(&y, 0x12345678);
   printf ("CSE write_32_rev: %s\n", y == 0x78563412 ? "ok" : "ERROR");
-
+  /* Make sure that ignoring the result of a builtin
+     doesn't cause an internal error */
+  (void) __builtin_bswap(x);
+  (void) __builtin_fsqrt(a);
   return 0;
 }
 
diff --git a/test/regression/builtins-ia32.c b/test/regression/builtins-ia32.c
index 10426209..558c3153 100644
--- a/test/regression/builtins-ia32.c
+++ b/test/regression/builtins-ia32.c
@@ -36,7 +36,10 @@ int main(int argc, char ** argv)
   y = 0;
   __builtin_write32_reversed(&y, 0x12345678);
   printf ("CSE write_32_rev: %s\n", y == 0x78563412 ? "ok" : "ERROR");
-
+  /* Make sure that ignoring the result of a builtin
+     doesn't cause an internal error */
+  (void) __builtin_bswap(x);
+  (void) __builtin_fsqrt(a);
   return 0;
 }
 
diff --git a/test/regression/builtins-powerpc.c b/test/regression/builtins-powerpc.c
index acffa435..90030737 100644
--- a/test/regression/builtins-powerpc.c
+++ b/test/regression/builtins-powerpc.c
@@ -50,7 +50,10 @@ int main(int argc, char ** argv)
   y = 0;
   __builtin_write32_reversed(&y, 0x12345678);
   printf ("CSE write_32_rev: %s\n", y == 0x78563412 ? "ok" : "ERROR");
-
+  /* Make sure that ignoring the result of a builtin
+     doesn't cause an internal error */
+  (void) __builtin_bswap(x);
+  (void) __builtin_fsqrt(a);
   return 0;
 }