diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml
index b12d60bb4226dc820850c208bff583fc9af6d702..100c72b114469d039af22b0fe2ea8b64fa9d0805 100644
--- a/cfrontend/C2Clight.ml
+++ b/cfrontend/C2Clight.ml
@@ -791,6 +791,13 @@ let atom_sizeof a =
   with Not_found ->
     None
 
+let atom_alignof a =
+  try
+    let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
+    Cutil.alignof env ty
+  with Not_found ->
+    None
+
 (** ** The builtin environment *)
 
 open Cparser.Builtins
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 65cd5b4fb2746ad62481de360d708265fab5bdf4..da64b565347a22fb98aeae9d075e425ffb3d8a35 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -64,6 +64,8 @@ let builtins = {
     "__builtin_sync",
       (TVoid [], [], false);
     "__builtin_isync",
+      (TVoid [], [], false);
+    "__builtin_trap",
       (TVoid [], [], false)
   ]
 }
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 31143fbbbb9c43dd41b3a29d83c211a6801fb928..f528335a634392b6aba47a8efbfdb021f5b3a780 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -219,6 +219,12 @@ let rolm_mask n =
   assert (!count = 2 || (!count = 0 && !last));
   (!mb, !me-1)
 
+(* Base-2 log of a Caml integer *)
+
+let rec log2 n =
+  assert (n > 0);
+  if n = 1 then 0 else 1 + log2 (n lsr 1)
+
 (* Built-in functions *)
 
 let re_builtin_function = Str.regexp "__builtin_"
@@ -310,6 +316,8 @@ let print_builtin_function oc s =
       fprintf oc "	sync\n"
   | "__builtin_isync" ->
       fprintf oc "	isync\n"
+  | "__builtin_trap" ->
+      fprintf oc "	trap\n"
   (* Catch-all *)
   | s ->
       invalid_arg ("unrecognized builtin function " ^ s)
@@ -610,7 +618,11 @@ let print_function oc name code =
   if not (C2Clight.atom_is_static name) then
     fprintf oc "	.globl %a\n" symbol name;
   fprintf oc "%a:\n" symbol name;
-  List.iter (print_instruction oc (labels_of_code Labelset.empty code)) code
+  List.iter (print_instruction oc (labels_of_code Labelset.empty code)) code;
+  if target <> MacOS then begin
+    fprintf oc "	.type	%a, @function\n" symbol name;
+    fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
+  end
 
 (* Generation of stub functions *)
 
@@ -816,13 +828,21 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
             if C2Clight.atom_is_readonly name
             then const_data
             else data
+      and align =
+        match C2Clight.atom_alignof name with
+        | Some a -> log2 a
+        | None -> 3 (* 8-alignment is a safe default *)
       in
       section oc sec;
-      fprintf oc "	.align	3\n";
+      fprintf oc "	.align	%d\n" align;
       if not (C2Clight.atom_is_static name) then
         fprintf oc "	.globl	%a\n" symbol name;
       fprintf oc "%a:\n" symbol name;
-      print_init_data oc name init_data
+      print_init_data oc name init_data;
+      if target <> MacOS then begin
+        fprintf oc "	.type	%a, @object\n" symbol name;
+        fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
+      end
 
 let print_program oc p =
   stubbed_functions := IdentSet.empty;