Merge branch 'debugscopes' into debug_locations

Conflicts:
	debug/CtoDwarf.ml
	debug/DwarfPrinter.ml

27 files changed, 342 insertions, 177 deletions

diff --git a/backend/Constprop.v b/backend/Constprop.v
index cd844d30..8f4cb76d 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -144,9 +144,9 @@ Fixpoint debug_strength_reduction (ae: AE.t) (al: list (builtin_arg reg)) :=
   | a :: al =>
       let a' := builtin_arg_reduction ae a in
       let al' := a :: debug_strength_reduction ae al in
-      match a' with
-      | BA_int _ | BA_long _ | BA_float _ | BA_single _ => a' :: al'
-      | _ => al'
+      match a, a' with
+      | BA _, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => a' :: al'
+      | _, _ => al'
       end
   end.
 
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index d9005f5e..eafefed5 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -243,7 +243,11 @@ Proof.
   induction 2; simpl.
 - exists (@nil val); constructor.
 - destruct IHlist_forall2 as (vl' & A).
-  destruct (builtin_arg_reduction ae a1); repeat (eauto; econstructor). 
+  assert (eval_builtin_args ge (fun r => rs#r) sp m
+             (a1 :: debug_strength_reduction ae al) (b1 :: vl'))
+  by (constructor; eauto).
+  destruct a1; try (econstructor; eassumption).
+  destruct (builtin_arg_reduction ae (BA x)); repeat (eauto; econstructor). 
 Qed.
 
 Lemma builtin_strength_reduction_correct:
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 2daa2d56..ed0fe524 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -266,6 +266,8 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args =
       args in
   match kind with
   | 1 ->  (* line number *)
+      fprintf oc "%s debug: current scopes%a\n"
+                 comment print_debug_args args;
       if Str.string_match re_file_line txt 0 then
         print_line oc (Str.matched_group 1 txt)
                       (int_of_string (Str.matched_group 2 txt))
@@ -280,6 +282,9 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args =
   | 5 ->  (* local variable preallocated in stack *)
       fprintf oc "%s debug: %s resides at%a\n"
                  comment txt print_debug_args args
+  | 6 ->  (* declaration of a local variable *)
+      fprintf oc "%s debug: %s declared in scope%a\n"
+                 comment txt print_debug_args args
   | _ ->
       ()
 					    
diff --git a/backend/RTL.v b/backend/RTL.v
index 56a5efeb..3cd4335d 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -104,8 +104,7 @@ Record function: Type := mkfunction {
     for its stack-allocated activation record.  [fn_params] is the list
     of registers that are bound to the values of arguments at call time.
     [fn_entrypoint] is the node of the first instruction of the function
-    in the CFG.  [fn_code_wf] asserts that all instructions of the function
-    have nodes no greater than [fn_nextpc]. *)
+    in the CFG. *)
 
 Definition fundef := AST.fundef function.
 
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/cfrontend/C2C.ml b/cfrontend/C2C.ml
index b7012ef9..dd55e60f 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -746,6 +746,22 @@ let rec convertExpr env e =
   | C.ECompound(ty1, ie) ->
       unsupported "compound literals"; ezero
 
+  | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) ->
+      let (kind, args1) =
+        match args with
+        | {edesc = C.EConst(CInt(n,_,_))} :: args1 -> (n, args1)
+        | _ -> error "ill_formed __builtin_debug"; (0L, args) in
+      let (text, args2) =
+        match args1 with
+        | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2)
+        | {edesc = C.EVar id} :: args2 -> (id.name, args2)
+        | _ -> error "ill_formed __builtin_debug"; ("", args1) in
+      let targs2 = convertTypArgs env [] args2 in
+      Ebuiltin(
+        EF_debug(P.of_int64 kind, intern_string text,
+                 typlist_of_typelist targs2),
+        targs2, convertExprList env args2, convertTyp env e.etyp)
+ 
   | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) ->
       begin match args with
       | {edesc = C.EConst(CStr txt)} :: args1 ->
@@ -927,16 +943,6 @@ let rec contains_case s =
 
 (** Annotations for line numbers *)
 
-let add_lineno prev_loc this_loc s =
-  if !Clflags.option_g && prev_loc <> this_loc && this_loc <> Cutil.no_loc
-  then begin
-    let txt = sprintf "#line:%s:%d" (fst this_loc) (snd this_loc) in
-     Ssequence(Sdo(Ebuiltin(EF_debug(P.one, intern_string txt, []),
-                            Tnil, Enil, Tvoid)),
-               s)
-  end else
-    s
-
 (** Statements *)
 
 let swrap = function
@@ -944,36 +950,31 @@ let swrap = function
   | Errors.Error msg ->
       error ("retyping error: " ^  string_of_errmsg msg); Sskip
 
-let rec convertStmt ploc env s =
+let rec convertStmt env s =
   updateLoc s.sloc;
   match s.sdesc with
   | C.Sskip ->
       Sskip
   | C.Sdo e ->
-      add_lineno ploc s.sloc (swrap (Ctyping.sdo (convertExpr env e)))
+      swrap (Ctyping.sdo (convertExpr env e))
   | C.Sseq(s1, s2) ->
-      let s1' = convertStmt ploc env s1 in
-      let s2' = convertStmt s1.sloc env s2 in
+      let s1' = convertStmt env s1 in
+      let s2' = convertStmt env s2 in
       Ssequence(s1', s2')
   | C.Sif(e, s1, s2) ->
       let te = convertExpr env e in
-      add_lineno ploc s.sloc 
-        (swrap (Ctyping.sifthenelse te 
-                      (convertStmt s.sloc env s1) (convertStmt s.sloc env s2)))
+      swrap (Ctyping.sifthenelse te (convertStmt env s1) (convertStmt env s2))
   | C.Swhile(e, s1) ->
       let te = convertExpr env e in
-      add_lineno ploc s.sloc
-        (swrap (Ctyping.swhile te (convertStmt s.sloc env s1)))
+      swrap (Ctyping.swhile te (convertStmt env s1))
   | C.Sdowhile(s1, e) ->
       let te = convertExpr env e in
-      add_lineno ploc s.sloc
-        (swrap (Ctyping.sdowhile te (convertStmt s.sloc env s1)))
+      swrap (Ctyping.sdowhile te (convertStmt env s1))
   | C.Sfor(s1, e, s2, s3) ->
       let te = convertExpr env e in
-      add_lineno ploc s.sloc
-        (swrap (Ctyping.sfor
-                      (convertStmt s.sloc env s1) te
-                      (convertStmt s.sloc env s2) (convertStmt s.sloc env s3)))
+      swrap (Ctyping.sfor
+                  (convertStmt env s1) te
+                  (convertStmt env s2) (convertStmt env s3))
   | C.Sbreak ->
       Sbreak
   | C.Scontinue ->
@@ -986,22 +987,20 @@ let rec convertStmt ploc env s =
           contains_case init
         end;
       let te = convertExpr env e in
-      add_lineno ploc s.sloc
-        (swrap (Ctyping.sswitch te
-                    (convertSwitch s.sloc env (is_longlong env e.etyp) cases)))
+      swrap (Ctyping.sswitch te
+               (convertSwitch env (is_longlong env e.etyp) cases))
   | C.Slabeled(C.Slabel lbl, s1) ->
-      add_lineno ploc s.sloc
-        (Slabel(intern_string lbl, convertStmt s.sloc env s1))
+      Slabel(intern_string lbl, convertStmt env s1)
   | C.Slabeled(C.Scase _, _) ->
       unsupported "'case' outside of 'switch'"; Sskip
   | C.Slabeled(C.Sdefault, _) ->
       unsupported "'default' outside of 'switch'"; Sskip
   | C.Sgoto lbl ->
-      add_lineno ploc s.sloc (Sgoto(intern_string lbl))
+      Sgoto(intern_string lbl)
   | C.Sreturn None ->
-      add_lineno ploc s.sloc (Sreturn None)
+      Sreturn None
   | C.Sreturn(Some e) ->
-      add_lineno ploc s.sloc (Sreturn(Some(convertExpr env e)))
+      Sreturn(Some(convertExpr env e))
   | C.Sblock _ ->
       unsupported "nested blocks"; Sskip
   | C.Sdecl _ ->
@@ -1009,10 +1008,9 @@ let rec convertStmt ploc env s =
   | C.Sasm(attrs, txt, outputs, inputs, clobber) ->
       if not !Clflags.option_finline_asm then
         unsupported "inline 'asm' statement (consider adding option -finline-asm)";
-      add_lineno ploc s.sloc
-        (Sdo (convertAsm s.sloc env txt outputs inputs clobber))
+      Sdo (convertAsm s.sloc env txt outputs inputs clobber)
 
-and convertSwitch ploc env is_64 = function
+and convertSwitch env is_64 = function
   | [] ->
       LSnil
   | (lbl, s) :: rem ->
@@ -1029,7 +1027,7 @@ and convertSwitch ploc env is_64 = function
                               then Z.of_uint64 v
                               else Z.of_uint32 (Int64.to_int32 v))
       in
-      LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env is_64 rem)
+      LScons(lbl', convertStmt env s, convertSwitch env is_64 rem)
 
 (** Function definitions *)
 
@@ -1057,7 +1055,7 @@ let convertFundef loc env fd =
         Debug.atom_local_variable id id';
         (id', convertTyp env ty))
       fd.fd_locals in
-  let body' = convertStmt loc env fd.fd_body in
+  let body' = convertStmt env fd.fd_body in
   let id' = intern_string fd.fd_name.name in
   Debug.atom_function fd.fd_name id';
   Hashtbl.add decl_atom id'
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index a555f792..1f55da7f 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -802,13 +802,13 @@ Program Definition composite_of_def
 Next Obligation.
   apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. 
   apply align_le; apply alignof_composite_pos.
-Qed.
+Defined.
 Next Obligation.
   apply align_attr_two_p. apply alignof_composite_two_p.
-Qed.
+Defined.
 Next Obligation.
   apply align_divides. apply alignof_composite_pos.
-Qed.
+Defined.
 
 (** The composite environment for a program is obtained by entering
   its composite definitions in sequence.  The definitions are assumed
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index cae56f00..d064f4b1 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -111,16 +111,16 @@ let pack_bitfields env sid ml =
           end
   in pack [] 0 ml
 
-let rec transf_members env id count = function
+let rec transf_struct_members env id count = function
   | [] -> []
   | m :: ms as ml ->
       if m.fld_bitfield = None then
-        m :: transf_members env id count ms
+        m :: transf_struct_members env id count ms
       else begin
         let (nbits, bitfields, ml') = pack_bitfields env id ml in
         if nbits = 0 then
           (* Lone zero-size bitfield: just ignore *)
-          transf_members env id count ml'
+          transf_struct_members env id count ml'
         else begin
           (* Create integer field of sufficient size for this bitfield group *)
           let carrier = sprintf "__bf%d" count in
@@ -144,14 +144,49 @@ let rec transf_members env id count = function
               end)
             bitfields;
           { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
-          :: transf_members env id (count + 1) ml'
+          :: transf_struct_members env id (count + 1) ml'
         end
       end
 
+let rec transf_union_members env id count = function
+    [] -> []
+  | m :: ms ->
+      (match m.fld_bitfield with
+      | None ->  m::transf_union_members env id count ms
+      | Some nbits ->
+          let carrier = sprintf "__bf%d" count in
+          let carrier_ikind = unsigned_ikind_for_carrier nbits in
+          let carrier_typ = TInt(carrier_ikind, []) in
+          let signed =
+            match unroll env m.fld_typ with
+            | TInt(ik, _) -> is_signed_ikind ik
+            | TEnum(eid, _) -> is_signed_enum_bitfield env id m.fld_name eid nbits
+            | _ -> assert false (* should never happen, checked in Elab *) in
+          let signed2 =
+            match unroll env (type_of_member env m) with
+            | TInt(ik, _) -> is_signed_ikind ik
+            | _ -> assert false (* should never happen, checked in Elab *) in
+          let pos' =
+            if !config.bitfields_msb_first
+            then sizeof_ikind carrier_ikind * 8 - nbits
+            else 0 in
+          let is_bool =
+            match unroll env m.fld_typ with
+            | TInt(IBool, _) -> true
+            | _ -> false in
+          Hashtbl.add bitfield_table
+            (id, m.fld_name)
+            {bf_carrier = carrier; bf_carrier_typ = carrier_typ;
+             bf_pos = pos'; bf_size = nbits;
+             bf_signed = signed; bf_signed_res = signed2;
+             bf_bool = is_bool};
+          { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
+          :: transf_struct_members env id (count + 1) ms)
+
 let transf_composite env su id attr ml =
   match su with
-  | Struct -> (attr, transf_members env id 1 ml)
-  | Union  -> (attr, ml)
+  | Struct -> (attr, transf_struct_members env id 1 ml)
+  | Union  -> (attr, transf_union_members env id 1 ml)
 
 (* Bitfield manipulation expressions *)
 
@@ -318,6 +353,7 @@ let rec is_bitfield_access env e =
   match e.edesc with
   | EUnop(Odot fieldname, e1) ->
       begin match unroll env e1.etyp with
+      | TUnion (id,_)
       | TStruct(id, _) ->
           (try Some(e1, Hashtbl.find bitfield_table (id, fieldname))
            with Not_found -> None)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index e802085d..021dc512 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1839,7 +1839,7 @@ let enter_or_refine_ident local loc env s sto ty =
 let enter_decdefs local loc env sto dl =
   (* Sanity checks on storage class *)
   if sto = Storage_register && not local then
-    error loc "'register' on global declaration";
+    fatal_error loc "'register' on global declaration";
   if sto <> Storage_default && dl = [] then
     warning loc "Storage class specifier on empty declaration";
   let rec enter_decdef (decls, env) (s, ty, init) =
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 91f50552..b5f945d4 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -177,74 +177,173 @@ and expand_init islocal env i =
   in
     expand i
 
+(* Insertion of debug annotation, for -g mode *)
+
+let debug_id = Env.fresh_ident "__builtin_debug"
+let debug_ty =
+  TFun(TVoid [], Some [Env.fresh_ident "kind", TInt(IInt, [])], true, [])
+
+let debug_annot kind args =
+  { sloc = no_loc;
+    sdesc = Sdo { 
+      etyp = TVoid [];
+      edesc = ECall({edesc = EVar debug_id; etyp = debug_ty},
+                    intconst kind IInt :: args)
+    }
+  }
+
+let string_const str =
+  let c = CStr str in { edesc = EConst c; etyp = type_of_constant c }
+
+let integer_const n =
+  intconst (Int64.of_int n) IInt
+
+(* Line number annotation:
+      __builtin_debug(1, "#line:filename:lineno", scope1, ..., scopeN) *)
+(* TODO: consider
+      __builtin_debug(1, "filename", lineno, scope1, ..., scopeN)
+   instead. *)
+
+let debug_lineno ctx (filename, lineno) =
+  debug_annot 1L
+    (string_const (Printf.sprintf "#line:%s:%d" filename lineno) ::
+     List.rev_map integer_const ctx)
+
+let add_lineno ctx prev_loc this_loc s =
+  if !Clflags.option_g && this_loc <> prev_loc && this_loc <> no_loc
+  then sseq no_loc (debug_lineno ctx this_loc) s
+  else s
+
+(* Variable declaration annotation:
+      __builtin_debug(6, var, scope)  *)
+
+let debug_var_decl ctx id ty =
+  let scope = match ctx with [] -> 0 | sc :: _ -> sc in
+  debug_annot 6L
+    [ {edesc = EVar id; etyp = ty}; integer_const scope ]
+
+let add_var_decl ctx id ty s =
+  if !Clflags.option_g
+  then sseq no_loc (debug_var_decl ctx id ty) s
+  else s
+
+let add_param_decls params body =
+  if !Clflags.option_g then
+    List.fold_right
+      (fun (id, ty) s -> sseq no_loc (debug_var_decl [] id ty) s)
+      params body
+  else body
+
+(* Generate fresh scope identifiers, for blocks that contain at least
+   one declaration *)
+
+let block_contains_decl sl =
+  List.exists
+    (function {sdesc = Sdecl _} -> true | _ -> false)
+    sl
+
+let next_scope_id = ref 0
+
+let new_scope_id () =
+  incr next_scope_id; !next_scope_id
+
 (* Process a block-scoped variable declaration.
    The variable is entered in [local_variables].
    The initializer, if any, is converted into assignments and
    prepended to [k]. *)
 
-let process_decl loc env (sto, id, ty, optinit) k =
+let process_decl loc env ctx (sto, id, ty, optinit) k =
   let ty' = remove_const env ty in
   local_variables := (sto, id, ty', None) :: !local_variables;
-  match optinit with
-  | None -> k
-  | Some init ->
-      let init' = expand_init true env init in
-      let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in
-      add_inits_stmt loc l k
+  add_var_decl ctx id ty
+   (match optinit with
+    | None ->
+        k
+    | Some init ->
+        let init' = expand_init true env init in
+        let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in
+        add_inits_stmt loc l k)
 
 (* Simplification of blocks within a statement *)
 
-let rec unblock_stmt env s =
+let rec unblock_stmt env ctx ploc s =
   match s.sdesc with
   | Sskip -> s
   | Sdo e ->
-      {s with sdesc = Sdo(expand_expr true env e)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sdo(expand_expr true env e)}
   | Sseq(s1, s2) ->
-      {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)}
+      {s with sdesc = Sseq(unblock_stmt env ctx ploc s1,
+                           unblock_stmt env ctx s1.sloc s2)}
   | Sif(e, s1, s2) -> 
-      {s with sdesc = Sif(expand_expr true env e,
-                          unblock_stmt env s1, unblock_stmt env s2)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sif(expand_expr true env e,
+                            unblock_stmt env ctx s.sloc s1,
+                            unblock_stmt env ctx s.sloc s2)}
   | Swhile(e, s1) -> 
-      {s with sdesc = Swhile(expand_expr true env e, unblock_stmt env s1)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Swhile(expand_expr true env e,
+                               unblock_stmt env ctx s.sloc s1)}
   | Sdowhile(s1, e) ->
-      {s with sdesc = Sdowhile(unblock_stmt env s1, expand_expr true env e)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sdowhile(unblock_stmt env ctx s.sloc s1,
+                                 expand_expr true env e)}
   | Sfor(s1, e, s2, s3) ->
-      {s with sdesc = Sfor(unblock_stmt env s1,
-                           expand_expr true env e,
-                           unblock_stmt env s2,
-                           unblock_stmt env s3)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sfor(unblock_stmt env ctx s.sloc s1,
+                             expand_expr true env e,
+                             unblock_stmt env ctx s.sloc s2,
+                             unblock_stmt env ctx s.sloc s3)}
   | Sbreak -> s
   | Scontinue -> s
   | Sswitch(e, s1) ->
-      {s with sdesc = Sswitch(expand_expr true env e, unblock_stmt env s1)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sswitch(expand_expr true env e,
+                                unblock_stmt env ctx s.sloc s1)}
   | Slabeled(lbl, s1) -> 
-      {s with sdesc = Slabeled(lbl, unblock_stmt env s1)}
-  | Sgoto lbl -> s
-  | Sreturn None -> s
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)}
+  | Sgoto lbl ->
+      add_lineno ctx ploc s.sloc s
+  | Sreturn None ->
+      add_lineno ctx ploc s.sloc s
   | Sreturn (Some e) ->
-      {s with sdesc = Sreturn(Some (expand_expr true env e))}
-  | Sblock sl -> unblock_block env sl
-  | Sdecl d -> assert false
+      add_lineno ctx ploc s.sloc 
+        {s with sdesc = Sreturn(Some (expand_expr true env e))}
+  | Sblock sl ->
+      let ctx' =
+        if block_contains_decl sl
+        then new_scope_id () :: ctx
+        else ctx in
+      unblock_block env ctx' ploc sl
+  | Sdecl d ->
+      assert false
   | Sasm(attr, template, outputs, inputs, clob) ->
       let expand_asm_operand (lbl, cstr, e) =
         (lbl, cstr, expand_expr true env e) in
-      {s with sdesc = Sasm(attr, template,
-                           List.map expand_asm_operand outputs,
-                           List.map expand_asm_operand inputs, clob)}
+      add_lineno ctx ploc s.sloc 
+        {s with sdesc = Sasm(attr, template,
+                             List.map expand_asm_operand outputs,
+                             List.map expand_asm_operand inputs, clob)}
 
 
-and unblock_block env = function
+and unblock_block env ctx ploc = function
   | [] -> sskip
   | {sdesc = Sdecl d; sloc = loc} :: sl ->
-      process_decl loc env d (unblock_block env sl)
+      add_lineno ctx ploc loc
+        (process_decl loc env ctx d
+           (unblock_block env ctx loc sl))
   | s :: sl ->
-      sseq s.sloc (unblock_stmt env s) (unblock_block env sl)
+      sseq s.sloc (unblock_stmt env ctx ploc s)
+                  (unblock_block env ctx s.sloc sl)
 
 (* Simplification of blocks and compound literals within a function *)
 
 let unblock_fundef env f =
   local_variables := [];
-  let body = unblock_stmt env f.fd_body in
+  next_scope_id := 0;
+  let body =
+    add_param_decls f.fd_params (unblock_stmt env [] no_loc f.fd_body) in
   let decls = !local_variables in
   local_variables := [];
   { f with fd_locals = f.fd_locals @ decls; fd_body = body }
@@ -299,4 +398,5 @@ let rec unblock_glob env accu = function
 (* Entry point *)
 
 let program p =
+  {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} ::
   unblock_glob (Builtins.environment()) [] p
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index a0b16463..5e58e365 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -58,6 +58,8 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
 
     let add_byte_size = add_abbr_entry (0xb,byte_size_type_abbr)
 
+    let add_member_size = add_abbr_entry (0xb,member_size_abbr)
+
     let add_high_pc = add_abbr_entry (0x12,high_pc_type_abbr)
 
     let add_low_pc = add_abbr_entry (0x11,low_pc_type_abbr)
@@ -153,7 +155,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       | DW_TAG_structure_type e ->
           prologue 0x13;
           add_attr_some e.structure_file_loc add_file_loc;
-          add_attr_some e.structure_byte_size add_byte_size;
+          add_attr_some e.structure_byte_size add_member_size;
           add_attr_some e.structure_declaration add_declaration;
           add_attr_some e.structure_name add_name
       | DW_TAG_subprogram e ->
@@ -184,7 +186,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       | DW_TAG_union_type e ->
           prologue 0x17;
           add_attr_some e.union_file_loc add_file_loc;
-          add_attr_some e.union_byte_size add_byte_size;
+          add_attr_some e.union_byte_size add_member_size;
           add_attr_some e.union_declaration add_declaration;
           add_attr_some e.union_name add_name
       | DW_TAG_unspecified_parameter e ->
@@ -246,7 +248,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
         fprintf oc "	.uleb128	%d\n" id;
         output_string oc s;
         fprintf oc "	.uleb128	0\n";
-        fprintf oc "	.uleb128	0\n")  abbrevs;
+        fprintf oc "	.uleb128	0\n\n")  abbrevs;
       fprintf oc "	.sleb128	0\n"
 
     let debug_start_addr = ref (-1)
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index eb7d4060..b5be3121 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -242,6 +242,7 @@ module type DWARF_ABBREVS =
     val name_type_abbr: int
     val encoding_type_abbr: int
     val byte_size_type_abbr: int
+    val member_size_abbr: int
     val high_pc_type_abbr: int
     val low_pc_type_abbr: int
     val stmt_list_type_abbr: int
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml
index d5e72adb..4cd838b6 100644
--- a/debug/DwarfUtil.ml
+++ b/debug/DwarfUtil.ml
@@ -85,6 +85,7 @@ module DefaultAbbrevs =
     let name_type_abbr = dw_form_string
     let encoding_type_abbr = dw_form_data1
     let byte_size_type_abbr = dw_form_data1
+    let member_size_abbr = dw_form_udata
     let high_pc_type_abbr = dw_form_addr
     let low_pc_type_abbr = dw_form_addr
     let stmt_list_type_abbr = dw_form_data4
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 863ed6a1..3c7bdd15 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -142,7 +142,7 @@ Inductive instruction : Type :=
   | Paddic: ireg -> ireg -> constant -> instruction           (**r add immediate and set carry *)
   | Paddis: ireg -> ireg -> constant -> instruction           (**r add immediate high *)
   | Paddze: ireg -> ireg -> instruction                       (**r add carry *)
-  | Pallocframe: Z -> int -> instruction                      (**r allocate new stack frame (pseudo) *)
+  | Pallocframe: Z -> int -> int -> instruction               (**r allocate new stack frame (pseudo) *)
   | Pand_: ireg -> ireg -> ireg -> instruction                (**r bitwise and *)
   | Pandc: ireg -> ireg -> ireg -> instruction                (**r bitwise and-complement *)
   | Pandi_: ireg -> ireg -> constant -> instruction           (**r and immediate and set conditions *)
@@ -157,6 +157,7 @@ Inductive instruction : Type :=
   | Pblr: instruction                                         (**r branch to contents of register LR *)
   | Pbt: crbit -> label -> instruction                        (**r branch if true *)
   | Pbtbl: ireg -> list label -> instruction                  (**r N-way branch through a jump table (pseudo) *)
+  | Pcmpb: ireg -> ireg -> ireg -> instruction                (**r compare bytes *)
   | Pcmplw: ireg -> ireg -> instruction                       (**r unsigned integer comparison *)
   | Pcmplwi: ireg -> constant -> instruction                  (**r same, with immediate argument *)
   | Pcmpw: ireg -> ireg -> instruction                        (**r signed integer comparison *)
@@ -206,6 +207,7 @@ Inductive instruction : Type :=
   | Pfrsqrte: freg -> freg -> instruction                     (**r approximate reciprocal of square root *)
   | Pfres: freg -> freg -> instruction                        (**r approximate inverse *)
   | Pfsel: freg -> freg -> freg -> freg -> instruction        (**r FP conditional move *)
+  | Pisel: ireg -> ireg -> ireg -> crbit -> instruction       (**r integer select *)
   | Pisync: instruction                                       (**r ISYNC barrier *)
   | Picbi: ireg -> ireg -> instruction                        (**r instruction cache invalidate *)
   | Picbtls: int -> ireg -> ireg -> instruction               (**r instruction cache block touch and lock set *)
@@ -323,7 +325,7 @@ lbl:    .double floatcst
         lfd     rdst, 0(r1)
         addi    r1, r1, 8
 >>
-- [Pallocframe sz ofs]: in the formal semantics, this pseudo-instruction
+- [Pallocframe sz ofs retofs]: in the formal semantics, this pseudo-instruction
   allocates a memory block with bounds [0] and [sz], stores the value
   of register [r1] (the stack pointer, by convention) at offset [ofs]
   in this block, and sets [r1] to a pointer to the bottom of this
@@ -622,7 +624,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Paddze rd r1 =>
       Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY)
                        #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m
-  | Pallocframe sz ofs =>
+  | Pallocframe sz ofs _ =>
       let (m1, stk) := Mem.alloc m 0 sz in
       let sp := Vptr stk Int.zero in
       match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with
@@ -871,6 +873,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   (** The following instructions and directives are not generated
       directly by [Asmgen], so we do not model them. *)
   | Pbdnz _
+  | Pcmpb _ _ _
   | Pcntlzw _ _
   | Pcreqv _ _ _
   | Pcrxor _ _ _
@@ -891,6 +894,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfrsqrte _ _
   | Pfres _ _
   | Pfsel _ _ _ _
+  | Pisel _ _ _ _
   | Plwarx _ _ _
   | Plwbrx _ _ _
   | Picbi _ _
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 5f875ebf..a7e66701 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -152,7 +152,7 @@ let p_instruction oc ic =
   | Paddic  (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
   | Paddis  (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddis\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
   | Paddze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Paddze\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
-  | Pallocframe (c,i) -> assert false(* Should not occur *)
+  | Pallocframe (c,i,r) -> assert false(* Should not occur *)
   | Pand_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pand_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pandc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pandc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pandi_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandi_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
@@ -167,6 +167,7 @@ let p_instruction oc ic =
   | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}"
   | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l
   | Pbtbl (i,lb) -> fprintf oc "{\"Instruction Name\":\"Pbtl\",\"Args\":[%a%a]}" p_ireg i (p_list_cont p_label) lb
+  | Pcmpb (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pcmpb\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pcmplw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmplw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pcmplwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmplwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c
   | Pcmpw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmpw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
@@ -216,6 +217,7 @@ let p_instruction oc ic =
   | Pfrsqrte (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrte\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
   | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
   | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4
+  | Pisel (ir1,ir2,ir3,cr) -> fprintf oc "{\"Instruction Name\":\"Pisel\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 p_crbit cr
   | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Picbtls (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbtls\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2
   | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}"
@@ -286,7 +288,7 @@ let p_instruction oc ic =
   | Pstwx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pstwux (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwux\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pstwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
-  | Pstwcx_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwc_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
+  | Pstwcx_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwcx_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Psubfc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Psubfe (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Psubfze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 3e57cdbf..b9fe1d7f 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -276,6 +276,9 @@ let expand_builtin_vstore chunk args =
       assert false
 
 (* Handling of varargs *)
+let linkregister_offset = ref  Int.zero
+
+let retaddr_offset = ref Int.zero
 
 let current_function_stacksize = ref 0l
 
@@ -324,56 +327,6 @@ let expand_builtin_va_start r =
 let expand_int64_arith conflict rl fn =
   if conflict then (fn GPR0; emit (Pmr(rl, GPR0))) else fn rl
 
-(* Handling of cache instructions *)
-
-(* Auxiliary function to generate address for the cache function *)
-let expand_builtin_cache_common addr f =
-  let add = match addr with
-  | BA (IR a1) -> a1
-  | BA_addrstack ofs ->
-      emit_addimm GPR11 GPR1 ofs;
-      GPR11
-  | BA_addrglobal(id, ofs) ->
-      if symbol_is_small_data id ofs then begin
-        emit (Paddi (GPR11, GPR0, Csymbol_sda(id, ofs)));
-        GPR11
-      end else if symbol_is_rel_data id ofs then begin
-        emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs)));
-        emit (Paddi(GPR11, GPR11, Csymbol_rel_low(id, ofs)));
-        GPR11
-      end else begin
-        emit (Paddis(GPR11, GPR0, Csymbol_high(id, ofs)));
-        emit (Paddi (GPR11, GPR11, Csymbol_low(id, ofs)));
-        GPR11
-      end 
-  | _ -> raise (Error "Argument is not an address") in
-  f add
- 
-let expand_builtin_prefetch addr rw loc =
-  if not ((loc >= _0) && (loc <= _2)) then
-    raise (Error "the last argument of __builtin_prefetch must be a constant between 0 and 2");
-  let emit_prefetch_instr addr =
-    if Int.eq rw _0 then begin
-      emit (Pdcbt (loc,GPR0,addr));
-    end else if Int.eq rw _1 then begin
-      emit (Pdcbtst (loc,GPR0,addr));
-    end else
-      raise (Error "the second argument of __builtin_prefetch must be either 0 or 1")
-  in
-  expand_builtin_cache_common addr emit_prefetch_instr
-
-let expand_builtin_dcbtls addr loc =
-  if not ((loc == _0) || (loc = _2)) then
-    raise (Error "the second argument of __builtin_dcbtls must be a constant between 0 and 2");
-  let emit_inst addr = emit (Pdcbtls (loc,GPR0,addr)) in
-  expand_builtin_cache_common addr emit_inst
-
-let expand_builtin_icbtls addr loc =
-  if not ((loc == _0) || (loc = _2)) then
-    raise (Error "the second argument of __builtin_icbtls must be a constant between 0 and 2");
-  let emit_inst addr = emit (Picbtls (loc,GPR0,addr)) in
-  expand_builtin_cache_common addr emit_inst
-
 (* Handling of compiler-inlined builtins *)
 
 let expand_builtin_inline name args res =
@@ -386,6 +339,8 @@ let expand_builtin_inline name args res =
       emit (Pmulhwu(res, a1, a2))
   | "__builtin_clz", [BA(IR a1)], BR(IR res) ->
       emit (Pcntlzw(res, a1))
+  | "__builtin_cmpb",  [BA(IR a1); BA(IR a2)], BR(IR res) ->
+      emit (Pcmpb (res,a1,a2))
   | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
       emit (Pstwu(a1, Cint _m8, GPR1));
       emit (Pcfi_adjust _8);
@@ -468,7 +423,7 @@ let expand_builtin_inline name args res =
       emit (Plwsync)
   | "__builtin_mbar",  [BA_int mo], _ ->
       if not (mo = _0 || mo = _1) then
-        raise (Error "the argument of __builtin_mbar must be either 0 or 1");
+        raise (Error "the argument of __builtin_mbar must be 0 or 1");
       emit (Pmbar mo)
   | "__builin_mbar",_, _ ->
       raise (Error "the argument of __builtin_mbar must be a constant");
@@ -484,16 +439,27 @@ let expand_builtin_inline name args res =
       emit (Pdcbi (GPR0,a1))
   | "__builtin_icbi", [BA(IR a1)],_ ->
       emit (Picbi(GPR0,a1))
-  | "__builtin_dcbtls", [a; BA_int loc],_ ->
-     expand_builtin_dcbtls a loc
+  | "__builtin_dcbtls", [BA (IR a1); BA_int loc],_ ->
+      if not ((Int.eq loc _0) || (Int.eq loc _2)) then
+        raise (Error "the second argument of __builtin_dcbtls must be 0 or 2");
+      emit (Pdcbtls (loc,GPR0,a1))    
   | "__builtin_dcbtls",_,_ ->
       raise (Error "the second argument of __builtin_dcbtls must be a constant")
-  | "__builtin_icbtls", [a; BA_int loc],_ ->
-     expand_builtin_icbtls a loc
+  | "__builtin_icbtls", [BA (IR a1); BA_int loc],_ ->
+    if not ((Int.eq loc _0) || (Int.eq loc _2)) then
+        raise (Error "the second argument of __builtin_icbtls must be 0 or 2");
+      emit (Picbtls (loc,GPR0,a1))
   | "__builtin_icbtls",_,_ ->
       raise (Error "the second argument of __builtin_icbtls must be a constant")
-  | "__builtin_prefetch" , [a1 ;BA_int rw; BA_int loc],_ ->
-      expand_builtin_prefetch a1 rw loc
+  | "__builtin_prefetch" , [BA (IR a1) ;BA_int rw; BA_int loc],_ ->
+      if not (Int.ltu loc _4) then
+        raise (Error "the last argument of __builtin_prefetch must be 0, 1 or 2");
+      if Int.eq rw _0 then begin
+        emit (Pdcbt (loc,GPR0,a1));
+      end else if Int.eq rw _1 then begin
+        emit (Pdcbtst (loc,GPR0,a1));
+      end else
+        raise (Error "the second argument of __builtin_prefetch must be 0 or 1")
   | "__builtin_prefetch" ,_,_ ->
       raise (Error "the second and third argument of __builtin_prefetch must be a constant")
   | "__builtin_dcbz",[BA (IR a1)],_ ->
@@ -507,6 +473,20 @@ let expand_builtin_inline name args res =
       emit (Pmtspr(n, a1))
   | "__builtin_set_spr", _, _ ->
       raise (Error "the first argument of __builtin_set_spr must be a constant")
+  (* Frame and return address *)
+  | "__builtin_call_frame", _,BR (IR res) ->
+      let sz = !current_function_stacksize 
+      and ofs = !linkregister_offset in
+      if sz < 0x8000l then
+        emit (Paddi(res, GPR1, Cint(coqint_of_camlint sz)))
+      else
+        emit (Plwz(res, Cint ofs, GPR1))
+  | "__builtin_return_address",_,BR (IR res) ->
+      emit (Plwz (res, Cint! retaddr_offset,GPR1))
+  (* isel *)
+  | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) ->
+      emit (Pcmpwi (a1,Cint (Int.zero)));
+      emit (Pisel (res,a3,a2,CRbit_2))
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
@@ -534,7 +514,7 @@ let num_crbit = function
 
 let expand_instruction instr =
   match instr with
-  | Pallocframe(sz, ofs) ->
+  | Pallocframe(sz, ofs,retofs) ->
       let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in
       let sz = camlint_of_coqint sz in
       assert (ofs = Int.zero);
@@ -553,7 +533,9 @@ let expand_instruction instr =
                   {sig_args = []; sig_res = None; sig_cc = cc_default}));
         emit (Pmtlr GPR0)
       end;
-      current_function_stacksize := sz
+      current_function_stacksize := sz;
+      linkregister_offset := ofs;
+      retaddr_offset := retofs
   | Pbctr sg | Pbctrl sg | Pbl(_, sg) | Pbs(_, sg) ->
       set_cr6 sg;
       emit instr
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 541fe7c6..db3b7028 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -711,7 +711,7 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo
 Definition transl_function (f: Mach.function) :=
   do c <- transl_code' f f.(Mach.fn_code) false;
   OK (mkfunction f.(Mach.fn_sig)
-       (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
+       (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) f.(fn_retaddr_ofs) ::
         Pmflr GPR0 ::
         Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
         Pcfi_rel_offset f.(fn_retaddr_ofs) :: c)).
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index e18fdb2d..1bb8c6f7 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -36,6 +36,8 @@ let builtins = {
       (TInt(IUInt, []), [TInt(IUInt, [])], false);
     "__builtin_bswap16",
       (TInt(IUShort, []), [TInt(IUShort, [])], false);
+    "__builtin_cmpb",
+      (TInt (IUInt, []),  [TInt(IUInt, []);TInt(IUInt, [])], false);
     (* Float arithmetic *)
     "__builtin_fmadd",
       (TFloat(FDouble, []), 
@@ -108,7 +110,15 @@ let builtins = {
     "__builtin_get_spr",
       (TInt(IUInt, []), [TInt(IInt, [])], false);
     "__builtin_set_spr",
-      (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false)
+      (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false);
+    (* Frame and return address *)
+    "__builtin_call_frame",
+      (TPtr (TVoid [],[]),[],false);
+    "__builtin_return_address",
+      (TPtr (TVoid [],[]),[],false);
+    (* isel *)
+    "__builtin_isel",
+      (TInt (IInt, []),[TInt(IBool, []);TInt(IInt, []);TInt(IInt, [])],false)
   ]
 }
 
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 402f07d1..a2017dca 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -217,9 +217,9 @@ Definition builtin_constraints (ef: external_function) :
   | EF_builtin id sg =>
       if ident_eq id builtin_get_spr then OK_const :: nil
       else if ident_eq id builtin_set_spr then OK_const :: OK_default :: nil
-      else if ident_eq id builtin_prefetch then OK_addrany :: OK_const :: OK_const :: nil
-      else if ident_eq id builtin_dcbtls then OK_addrany::OK_const::nil
-      else if ident_eq id builtin_icbtls then OK_addrany::OK_const::nil
+      else if ident_eq id builtin_prefetch then OK_default :: OK_const :: OK_const :: nil
+      else if ident_eq id builtin_dcbtls then OK_default::OK_const::nil
+      else if ident_eq id builtin_icbtls then OK_default::OK_const::nil
       else if ident_eq id builtin_mbar then OK_const::nil
       else nil
   | EF_vload _ => OK_addrany :: nil
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index c126f641..58117ee7 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -384,7 +384,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
       | Paddze(r1, r2) ->
           fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
-      | Pallocframe(sz, ofs) ->
+      | Pallocframe(sz, ofs, _) ->
           assert false
       | Pand_(r1, r2, r3) ->
           fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
@@ -443,6 +443,8 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	bctr\n";
           jumptables := (lbl, tbl) :: !jumptables;
           fprintf oc "%s end pseudoinstr btbl\n" comment
+      | Pcmpb (r1, r2, r3) ->
+          fprintf oc "	cmpb	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
       | Pcmplw(r1, r2) ->
           fprintf oc "	cmplw	%a, %a, %a\n" creg 0 ireg r1 ireg r2
       | Pcmplwi(r1, c) ->
@@ -537,6 +539,8 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fres	%a, %a\n" freg r1 freg r2    
       | Pfsel(r1, r2, r3, r4) ->
           fprintf oc "	fsel	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
+      | Pisel (r1,r2,r3,cr) ->
+          fprintf oc "	isel	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 crbit cr
       | Picbi (r1,r2) ->
           fprintf oc "	icbi	%a,%a\n" ireg r1 ireg r2
       | Picbtls (n,r1,r2) ->
diff --git a/test/c/aes.c b/test/c/aes.c
index abdaf6c3..88b3de4a 100644
--- a/test/c/aes.c
+++ b/test/c/aes.c
@@ -1423,7 +1423,7 @@ static void do_test(int keybits, u8 * key,
 static void do_bench(int nblocks)
 {
   u32 ckey[4 * (MAXNR + 1)];
-  u8 temp[16];
+  u8 temp[16] = "Plaintext";
   int nr;
 
   nr = rijndaelKeySetupEnc(ckey, (u8 *)"\x00\x01\x02\x03\x04\x05\x06\x07\x08\x09\x0A\x0B\x0C\x0D\x0E\x0F", 128);
diff --git a/test/regression/alias.c b/test/regression/alias.c
index a38e6dfd..9887ae2b 100644
--- a/test/regression/alias.c
+++ b/test/regression/alias.c
@@ -1,8 +1,8 @@
 /* Testing the alias analysis on ill-defined codes 
    where it should remain conservative. */
 
-typedef unsigned int uintptr_t;
-typedef signed int ptrdiff_t;
+#include <stddef.h>
+#include <stdint.h>
 
 /* For testing with GCC */
 #define NOINLINE __attribute__((noinline))
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;
 }