1 files changed, 11 insertions, 0 deletions
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index 868fb8df..657c4daa 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -86,6 +86,17 @@ let type_instr retty (Coq_pair(pc, i)) =
         raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s"
                                          name msg))
       end
+  | Ibuiltin(ef, args, res, _) ->
+      begin try
+        let sg = ef_sig ef in
+        set_types args sg.sig_args;
+        set_type res (match sg.sig_res with None -> Tint | Some ty -> ty);
+        if not (Conventions.arity_ok sg.sig_args) then
+          raise(Type_error "wrong arity")
+      with Type_error msg ->
+        raise(Type_error (Printf.sprintf "type mismatch in Ibuiltin(%s): %s"
+                                         (extern_atom ef.ef_id) msg))
+      end
   | Icond(cond, args, _, _) ->
       set_types args (type_of_condition cond)
   | Ijumptable(arg, _) ->