diff --git a/x86/Asm.v b/x86/Asm.v
index 58e28c4007..333f98a1e9 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -250,6 +250,7 @@ Inductive instruction: Type :=
   | Plabel(l: label)
   | Pallocframe(sz: Z)(ofs_ra ofs_link: ptrofs)
   | Pfreeframe(sz: Z)(ofs_ra ofs_link: ptrofs)
+  | Ptrap
   | Pbuiltin(ef: external_function)(args: list (builtin_arg preg))(res: builtin_res preg)
   (** Instructions not generated by [Asmgen] -- TO CHECK *)
   | Padcl_ri (rd: ireg) (n: int)
@@ -967,6 +968,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
               end
           end
       end
+  | Ptrap =>
+      Stuck
   | Pbuiltin ef args res =>
       Stuck                             (**r treated specially below *)
   (** The following instructions and directives are not generated
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index b835304611..5189bbef5b 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -476,6 +476,9 @@ let expand_builtin_inline name args res =
   (* no operation *)
   | "__builtin_nop", [], _ ->
      emit Pnop
+  (* Unconditional trap *)
+  | "__builtin_trap", [], _ ->
+     emit Ptrap
   (* Catch-all *)
   | _ ->
      raise (Error ("unrecognized builtin " ^ name))
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index e7f714c744..97feb8841d 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -73,6 +73,9 @@ let builtins = {
       (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
     "__builtin_write32_reversed",
       (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
+    (* Unconditional trap *)
+    "__builtin_trap",
+      (TVoid [], [], false);
   ]
 }
 
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 6159437ede..abde737ef1 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -815,6 +815,8 @@ module Target(System: SYSTEM):TARGET =
       | Pallocframe(sz, ofs_ra, ofs_link)
       | Pfreeframe(sz, ofs_ra, ofs_link) ->
 	 assert false
+      | Ptrap ->
+          fprintf oc "ud2\n"
       | Pbuiltin(ef, args, res) ->
           begin match ef with
             | EF_annot(kind,txt, targs) ->