Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

19 files changed, 89 insertions, 165 deletions

diff --git a/.gitattributes b/.gitattributes
new file mode 100644
index 00000000..02ab53c1
--- /dev/null
+++ b/.gitattributes
@@ -0,0 +1,3 @@
+# Files that should be ignored by Github linguist
+test/* linguist-vendored
+doc/* linguist-documentation
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 9ff2ae55..a64f4862 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -5,9 +5,9 @@ let rec make_identity_ptree_rec = function
 | [] -> PTree.empty
 | m::lm -> let (n, _) = m in PTree.set n n (make_identity_ptree_rec lm)
 
-let make_identity_ptree f = make_identity_ptree_rec (PTree.elements (fn_code f))
+let make_identity_ptree f = make_identity_ptree_rec (PTree.elements f.fn_code)
 
 (* For now, identity function *)
 let duplicate_aux f =
   let pTreeId = make_identity_ptree f
-  in (((fn_code f), (fn_entrypoint f)), pTreeId)
+  in ((f.fn_code, f.fn_entrypoint), pTreeId)
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 181f40bf..cc84b1cc 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -744,7 +744,7 @@ Lemma match_stacks_free_right:
   match_stacks F m m1' stk stk' sp.
 Proof.
   intros. eapply match_stacks_invariant; eauto.
-  intros. eapply Mem.perm_free_1; eauto.
+  intros. eapply Mem.perm_free_1; eauto with ordered_type.
   intros. eapply Mem.perm_free_3; eauto.
 Qed.
 
@@ -1043,7 +1043,7 @@ Proof.
   eapply match_stacks_bound with (bound := sp').
   eapply match_stacks_invariant; eauto.
     intros. eapply Mem.perm_free_3; eauto.
-    intros. eapply Mem.perm_free_1; eauto.
+    intros. eapply Mem.perm_free_1; eauto with ordered_type.
     intros. eapply Mem.perm_free_3; eauto.
   erewrite Mem.nextblock_free; eauto. red in VB; xomega.
   eapply agree_val_regs; eauto.
@@ -1135,7 +1135,7 @@ Proof.
   eapply match_stacks_bound with (bound := sp').
   eapply match_stacks_invariant; eauto.
     intros. eapply Mem.perm_free_3; eauto.
-    intros. eapply Mem.perm_free_1; eauto.
+    intros. eapply Mem.perm_free_1; eauto with ordered_type.
     intros. eapply Mem.perm_free_3; eauto.
   erewrite Mem.nextblock_free; eauto. red in VB; xomega.
   destruct or; simpl. apply agree_val_reg; auto. auto.
@@ -1182,7 +1182,7 @@ Proof.
     subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto.
     intros. eapply Mem.perm_alloc_1; eauto.
     intros. exploit Mem.perm_alloc_inv. eexact A. eauto.
-    rewrite dec_eq_false; auto.
+    rewrite dec_eq_false; auto with ordered_type.
   auto. auto. auto. eauto. auto.
   rewrite H5. apply agree_regs_init_regs. eauto. auto. inv H1; auto. congruence. auto.
   eapply Mem.valid_new_block; eauto.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 9c8cd5fc..0fa6838c 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -327,7 +327,7 @@ Local Opaque mreg_type.
     change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.
     red; intros; subst op. simpl in ISMOVE.
     destruct args; try discriminate. destruct args; discriminate.
-    apply wt_undef_regs; auto.
+    (* apply wt_undef_regs; auto. *)
 - (* load *)
   simpl in *; InvBooleans.
   econstructor; eauto.
diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
deleted file mode 100644
index 4e8efd16..00000000
--- a/backend/PrintLTLin.ml
+++ /dev/null
@@ -1,115 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Pretty-printer for LTLin code *)
-
-open Format
-open Camlcoq
-open Datatypes
-open Maps
-open AST
-open Integers
-open Locations
-open Machregsaux
-open LTLin
-open PrintAST
-open PrintOp
-
-let reg pp loc =
-  match loc with
-  | R r ->
-      begin match name_of_register r with
-      | Some s -> fprintf pp "%s" s
-      | None -> fprintf pp "<unknown reg>"
-      end
-  | S (Local(ofs, ty)) ->
-      fprintf pp "local(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
-  | S (Incoming(ofs, ty)) ->
-      fprintf pp "incoming(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
-  | S (Outgoing(ofs, ty)) ->
-      fprintf pp "outgoing(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
-
-let rec regs pp = function
-  | [] -> ()
-  | [r] -> reg pp r
-  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
-
-let ros pp = function
-  | Coq_inl r -> reg pp r
-  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
-
-let print_instruction pp i =
-  match i with
-  | Lop(op, args, res) ->
-      fprintf pp "%a = %a@ "
-         reg res (PrintOp.print_operation reg) (op, args)
-  | Lload(chunk, addr, args, dst) ->
-      fprintf pp "%a = %s[%a]@ "
-         reg dst (name_of_chunk chunk)
-         (PrintOp.print_addressing reg) (addr, args)
-  | Lstore(chunk, addr, args, src) ->
-      fprintf pp "%s[%a] = %a@ "
-         (name_of_chunk chunk)
-         (PrintOp.print_addressing reg) (addr, args)
-         reg src
-  | Lcall(sg, fn, args, res) ->
-      fprintf pp "%a = %a(%a)@ "
-        reg res ros fn regs args
-  | Ltailcall(sg, fn, args) ->
-      fprintf pp "tailcall %a(%a)@ "
-        ros fn regs args
-  | Lbuiltin(ef, args, res) ->
-      fprintf pp "%a = builtin %s(%a)@ "
-        reg res (name_of_external ef) regs args
-  | Llabel lbl ->
-      fprintf pp "%ld:@ " (P.to_int32 lbl)
-  | Lgoto lbl ->
-      fprintf pp "goto %ld@ " (P.to_int32 lbl)
-  | Lcond(cond, args, lbl) ->
-      fprintf pp "if (%a) goto %ld@ "
-        (PrintOp.print_condition reg) (cond, args)
-        (P.to_int32 lbl)
-  | Ljumptable(arg, tbl) ->
-      let tbl = Array.of_list tbl in
-      fprintf pp "@[<v 2>jumptable (%a)" reg arg;
-      for i = 0 to Array.length tbl - 1 do
-        fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i))
-      done;
-      fprintf pp "@]@ "
-  | Lreturn None ->
-      fprintf pp "return@ "
-  | Lreturn (Some arg) ->
-      fprintf pp "return %a@ " reg arg
-
-let print_function pp id f =
-  fprintf pp "@[<v 2>%s(%a) {@ " (extern_atom id) regs f.fn_params;
-  List.iter (print_instruction pp) f.fn_code;
-  fprintf pp "@;<0 -2>}@]@."
-
-let print_globdef pp (id, gd) =
-  match gd with
-  | Gfun(Internal f) -> print_function pp id f
-  | _ -> ()
-
-let print_program pp prog =
-  List.iter (print_globdef pp) prog.prog_defs
-
-let destination : string option ref = ref None
-
-let print_if prog =
-  match !destination with
-  | None -> ()
-  | Some f ->
-      let oc = open_out f in
-      let pp = formatter_of_out_channel oc in
-      print_program pp prog;
-      close_out oc
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 8dbb67a7..2b233900 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1148,10 +1148,10 @@ Proof.
 - constructor.
 - assert (Plt sp bound') by eauto with va.
   eapply sound_stack_public_call; eauto. apply IHsound_stack; intros.
-  apply INV. xomega. rewrite SAME; auto. xomega. auto. auto.
+  apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto.
 - assert (Plt sp bound') by eauto with va.
   eapply sound_stack_private_call; eauto. apply IHsound_stack; intros.
-  apply INV. xomega. rewrite SAME; auto. xomega. auto. auto.
+  apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto.
   apply bmatch_ext with m; auto. intros. apply INV. xomega. auto. auto. auto.
 Qed.
 
@@ -1362,7 +1362,7 @@ Proof.
   apply sound_stack_exten with bc.
   apply sound_stack_inv with m. auto.
   intros. apply Q. red. eapply Plt_trans; eauto.
-  rewrite C; auto.
+  rewrite C; auto with ordered_type.
   exact AA.
 * (* public builtin call *)
   exploit anonymize_stack; eauto.
@@ -1381,7 +1381,7 @@ Proof.
   apply sound_stack_exten with bc.
   apply sound_stack_inv with m. auto.
   intros. apply Q. red. eapply Plt_trans; eauto.
-  rewrite C; auto.
+  rewrite C; auto with ordered_type.
   exact AA.
   }
   unfold transfer_builtin in TR.
diff --git a/configure b/configure
index 9b5109b1..142222c4 100755
--- a/configure
+++ b/configure
@@ -568,14 +568,14 @@ missingtools=false
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
 case "$coq_ver" in
-  8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10)
+  8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires one of the following Coq versions: 8.10, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0"
+            echo "Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0"
             missingtools=true
         fi;;
   "")
@@ -587,15 +587,10 @@ esac
 echo "Testing OCaml... " | tr -d '\n'
 ocaml_ver=`ocamlopt -version 2>/dev/null`
 case "$ocaml_ver" in
-  4.00.*|4.01.*)
+  4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*)
         echo "version $ocaml_ver -- UNSUPPORTED"
-        echo "Error: CompCert requires OCaml version 4.02 or later."
+        echo "Error: CompCert requires OCaml version 4.05 or later."
         missingtools=true;;
-  4.02.*|4.03.*|4.04.*)
-      echo "version $ocaml_ver -- good!"
-      echo "WARNING: some Intel processors of the Skylake and Kaby Lake generations"
-      echo "have a hardware bug that can be triggered by this version of OCaml."
-      echo "To avoid this risk, it is recommended to use OCaml 4.05 or later.";;
   4.0*)
         echo "version $ocaml_ver -- good!";;
   ?.*)
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index 58dea5f4..ecf83779 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -271,7 +271,7 @@ let constant_expr env ty e =
   try
     match unroll env ty, cast env ty (expr env e) with
     | TInt(ik, _), I n -> Some(CInt(n, ik, ""))
-    | TPtr(_, _), I n -> Some(CInt(n, IInt, ""))
+    | TPtr(_, _), I n -> Some(CInt(n, ptr_t_ikind (), ""))
     | (TArray(_, _, _) | TPtr(_, _)), S s -> Some(CStr s)
     | (TArray(_, _, _) | TPtr(_, _)), WS s -> Some(CWStr s)
     | TEnum(_, _), I n -> Some(CInt(n, enum_ikind, ""))
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 7a2f4828..3467c092 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -836,6 +836,12 @@ let is_anonymous_composite = function
   | TUnion (id,_) -> id.C.name = ""
   | _ -> false
 
+let is_anonymous_type = function
+  | TEnum (id,_)
+  | TStruct (id,_)
+  | TUnion (id,_) -> id.C.name = ""
+  | _ -> false
+
 let is_function_pointer_type env t =
   match unroll env t with
   | TPtr (ty, _) -> is_function_type env ty
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index f6c4627d..2ddee78c 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -174,6 +174,8 @@ val is_function_pointer_type : Env.t -> typ -> bool
   (* Is type a pointer to function type? *)
 val is_anonymous_composite : typ -> bool
   (* Is type an anonymous composite? *)
+val is_anonymous_type : typ -> bool
+  (* Is the type an anonymous composite or enum *)
 val is_qualified_array : typ -> bool
   (* Does the type contain a qualified array type (e.g. int[const 5])? *)
 val pointer_arithmetic_ok : Env.t -> typ -> bool
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 3797164d..2b04340e 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -39,7 +39,16 @@ let warning loc =
 let print_typ env fmt ty =
   match ty with
   | TNamed _  ->
-      Format.fprintf fmt "'%a' (aka '%a')" Cprint.typ_raw ty Cprint.typ_raw (unroll env ty)
+    Format.fprintf fmt "'%a'" Cprint.typ_raw ty;
+    let ty' = unroll env ty in
+    if not (is_anonymous_type ty')
+    then Format.fprintf fmt " (aka '%a')" Cprint.typ_raw ty'
+  | TStruct (id,_) when id.C.name = "" ->
+    Format.fprintf fmt "'struct <anonymous>'"
+  | TUnion (id,_) when id.C.name = "" ->
+    Format.fprintf fmt "'union <anonymous>'"
+  | TEnum (id,_) when id.C.name = "" ->
+    Format.fprintf fmt "'enum <anonymous>'"
   | _ -> Format.fprintf fmt "'%a'" Cprint.typ_raw ty
 
 let pp_field fmt id =
@@ -172,7 +181,7 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty =
 	error loc "static declaration of '%s' follows non-static declaration" s;
         sto
     | Storage_static,_ -> Storage_static (* Static stays static *)
-    | Storage_extern,_ -> sto
+    | Storage_extern,_ -> if is_function_type env new_ty then Storage_extern else sto
     | Storage_default,Storage_extern ->
       if is_global_defined s && is_function_type env ty then
         warning loc Extern_after_definition "this extern declaration follows a non-extern definition and is ignored";
@@ -1056,7 +1065,7 @@ and elab_struct_or_union_info kind loc env members attrs =
   | fld :: rem ->
       if wrap incomplete_type loc env' fld.fld_typ then
         (* Must be fatal otherwise we get problems constructing the init *)
-        fatal_error loc "member '%a' has incomplete type" pp_field fld.fld_name;
+        fatal_error loc "member '%a' has incomplete type %a" pp_field fld.fld_name (print_typ env) fld.fld_typ;
       if wrap contains_flex_array_mem loc env' fld.fld_typ && kind = Struct then
         warning loc Flexible_array_extensions "%a may not be used as a struct member due to flexible array member" (print_typ env) fld.fld_typ;
       check_reduced_alignment loc env' fld.fld_typ;
@@ -1611,7 +1620,7 @@ end;
 try
   elab_item (I.top env root ty_root) ie []
 with No_default_init ->
-  error loc "variable has incomplete type %a" Cprint.typ ty_root;
+  error loc "variable has incomplete type %a" (print_typ env) ty_root;
   raise Exit
 
 (* Elaboration of a top-level initializer *)
@@ -1909,6 +1918,8 @@ let elab_expr ctx loc env a =
 
   | CAST ((spec, dcl), ie) ->
       let (ty, env) = elab_type loc env spec dcl in
+      if not (is_array_type env ty) && incomplete_type env ty then
+        fatal_error "ill-formed compound literal with incomplete type %a" (print_typ env) ty;
       begin match elab_initializer loc env "<compound literal>" ty ie with
       | (ty', Some i) -> { edesc = ECompound(ty', i); etyp = ty' },env
       | (ty', None)   -> fatal_error "ill-formed compound literal"
@@ -2425,9 +2436,10 @@ let enter_typedef loc env sto (s, ty, init) =
 
 let enter_decdef local nonstatic_inline loc sto (decls, env) (s, ty, init) =
   let isfun = is_function_type env ty in
+  let has_init = init <> NO_INIT in
   if sto = Storage_register && has_std_alignas env ty then
     error loc "alignment specified for 'register' object '%s'" s;
-  if sto = Storage_extern && init <> NO_INIT then
+  if sto = Storage_extern && has_init then
     error loc "'extern' declaration variable has an initializer";
   if local && isfun then begin
     match sto with
@@ -2451,10 +2463,14 @@ let enter_decdef local nonstatic_inline loc sto (decls, env) (s, ty, init) =
      initializer can refer to the ident *)
   let (id, sto', env1, ty, linkage) =
     enter_or_refine_ident local loc env s sto1 ty in
-  if init <> NO_INIT && not local then
+  if has_init && not local then
     add_global_define loc s;
-  if not isfun && is_void_type env ty then
-    fatal_error loc "'%s' has incomplete type" s;
+  (* check if the type is void or incomplete and the declaration is initialized *)
+  if not isfun then begin
+    let incomplete_init = not (is_array_type env1 ty) && wrap incomplete_type loc env1 ty && has_init in
+    if is_void_type env1 ty || incomplete_init then
+      fatal_error loc "variable '%s' has incomplete type %a" s (print_typ env) ty;
+  end;
   (* process the initializer *)
   let (ty', init') = elab_initializer loc env1 s ty init in
   (* update environment with refined type *)
@@ -2465,7 +2481,7 @@ let enter_decdef local nonstatic_inline loc sto (decls, env) (s, ty, init) =
       warning loc Tentative_incomplete_static "tentative static definition with incomplete type";
     end
     else if local && sto' <> Storage_extern then
-      error loc "variable has incomplete type %a" (print_typ env) ty';
+      error loc "variable '%s' has incomplete type %a" s (print_typ env) ty';
   (* check if alignment is reduced *)
   check_reduced_alignment loc env ty';
   (* check for static variables in nonstatic inline functions *)
@@ -2659,10 +2675,10 @@ let elab_fundef genv spec name defs body loc =
      and additionally they should have an identifier. In both cases a fatal
      error is raised in order to avoid problems at later places. *)
   let add_param env (id, ty) =
-    if wrap incomplete_type loc env ty then
-      fatal_error loc "parameter has incomplete type";
     if id.C.name = "" then
       fatal_error loc "parameter name omitted";
+    if wrap incomplete_type loc env ty then
+      fatal_error loc "parameter '%s' has incomplete type %a" id.C.name (print_typ env) ty;
     Env.add_ident env id Storage_default ty
   in
   (* Enter parameters and extra declarations in the local environment.
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index b124586a..d86e137a 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -381,7 +381,7 @@ and lblstmts p = function
               (print_option coqZ) lbl stmt s lblstmts ls
 
 let print_function p (id, f) =
-  fprintf p "Definition f_%s := {|@ " (extern_atom id);
+  fprintf p "Definition f_%s := {|@ " (sanitize (extern_atom id));
   fprintf p "  fn_return := %a;@ " typ f.fn_return;
   fprintf p "  fn_callconv := %a;@ " callconv f.fn_callconv;
   fprintf p "  fn_params := %a;@ " (print_list (print_pair ident typ)) f.fn_params;
@@ -402,7 +402,7 @@ let init_data p = function
   | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqptrofs ofs
 
 let print_variable p (id, v) =
-  fprintf p "Definition v_%s := {|@ " (extern_atom id);
+  fprintf p "Definition v_%s := {|@ " (sanitize (extern_atom id));
   fprintf p "  gvar_info := %a;@ " typ v.gvar_info;
   fprintf p "  gvar_init := %a;@ " (print_list init_data) v.gvar_init;
   fprintf p "  gvar_readonly := %B;@ " v.gvar_readonly;
@@ -417,12 +417,12 @@ let print_globdef p (id, gd) =
 
 let print_ident_globdef p = function
   | (id, Gfun(Ctypes.Internal f)) ->
-      fprintf p "(%a, Gfun(Internal f_%s))" ident id (extern_atom id)
+      fprintf p "(%a, Gfun(Internal f_%s))" ident id (sanitize (extern_atom id))
   | (id, Gfun(Ctypes.External(ef, targs, tres, cc))) ->
       fprintf p "@[<hov 2>(%a,@ @[<hov 2>Gfun(External %a@ %a@ %a@ %a))@]@]"
         ident id external_function ef typlist targs typ tres callconv cc
   | (id, Gvar v) ->
-      fprintf p "(%a, Gvar v_%s)" ident id (extern_atom id)
+      fprintf p "(%a, Gvar v_%s)" ident id (sanitize (extern_atom id))
 
 (* Composite definitions *)
 
diff --git a/lib/Heaps.v b/lib/Heaps.v
index 9fa07a1d..85343998 100644
--- a/lib/Heaps.v
+++ b/lib/Heaps.v
@@ -256,14 +256,14 @@ Proof.
   eapply gt_heap_trans with y; eauto. red; auto.
 - intuition.
   eapply lt_heap_trans; eauto. red; auto.
-  eapply gt_heap_trans; eauto. red; auto.
+  eapply gt_heap_trans; eauto. red; auto with ordered_type.
 - intuition. eapply gt_heap_trans; eauto. red; auto.
 - rewrite e3 in *; simpl in *. intuition.
   eapply lt_heap_trans with y; eauto. red; auto.
   eapply gt_heap_trans; eauto. red; auto.
 - intuition.
   eapply lt_heap_trans with y; eauto. red; auto.
-  eapply gt_heap_trans; eauto. red; auto.
+  eapply gt_heap_trans; eauto. red; auto with ordered_type.
   eapply gt_heap_trans with x; eauto. red; auto.
 - rewrite e3 in *; simpl in *; intuition.
   eapply gt_heap_trans; eauto. red; auto.
@@ -308,7 +308,7 @@ Proof.
   intros. unfold insert.
   case_eq (partition x h). intros a b EQ; simpl.
   assert (E.eq y x \/ ~E.eq y x).
-    destruct (E.compare y x); auto.
+    destruct (E.compare y x); auto with ordered_type.
     right; red; intros. elim (E.lt_not_eq l). apply E.eq_sym; auto.
   destruct H0.
   tauto.
diff --git a/lib/Integers.v b/lib/Integers.v
index 3e78ee60..bc05a4da 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -3327,10 +3327,11 @@ Proof.
   assert (0 <= Z.min (size a) (size b)).
     generalize (size_range a) (size_range b). zify; omega.
   apply bits_size_3. auto. intros.
-  rewrite bits_and. zify. subst z z0. destruct H1.
-  rewrite (bits_size_2 a). auto. omega.
-  rewrite (bits_size_2 b). apply andb_false_r. omega.
-  omega.
+  rewrite bits_and by omega.
+  rewrite andb_false_iff.
+  generalize (bits_size_2 a i).
+  generalize (bits_size_2 b i).
+  zify; intuition.
 Qed.
 
 Corollary and_interval:
diff --git a/lib/IntvSets.v b/lib/IntvSets.v
index 78c20cc5..b97d9882 100644
--- a/lib/IntvSets.v
+++ b/lib/IntvSets.v
@@ -102,7 +102,7 @@ Proof.
   simpl. rewrite IHok. tauto.
   destruct (zlt h0 l).
   simpl. tauto.
-  rewrite IHok. intuition.
+  rewrite IHok. intuition idtac.
   assert (l0 <= x < h0 \/ l <= x < h) by xomega. tauto.
   left; xomega.
   left; xomega.
diff --git a/lib/Ordered.v b/lib/Ordered.v
index bcf24cbd..1adbd330 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -21,6 +21,8 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import Integers.
 
+Create HintDb ordered_type.
+
 (** The ordered type of positive numbers *)
 
 Module OrderedPositive <: OrderedType.
@@ -173,17 +175,17 @@ Definition eq (x y: t) :=
 
 Lemma eq_refl : forall x : t, eq x x.
 Proof.
-  intros; split; auto.
+  intros; split; auto with ordered_type.
 Qed.
 
 Lemma eq_sym : forall x y : t, eq x y -> eq y x.
 Proof.
-  unfold eq; intros. intuition auto.
+  unfold eq; intros. intuition auto with ordered_type.
 Qed.
 
 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
 Proof.
-  unfold eq; intros. intuition eauto.
+  unfold eq; intros. intuition eauto with ordered_type.
 Qed.
 
 Definition lt (x y: t) :=
@@ -201,7 +203,7 @@ Proof.
   case (A.compare (fst x) (fst z)); intro.
   assumption.
   generalize (A.lt_not_eq H2); intro. elim H5.
-  apply A.eq_trans with (fst z). auto. auto.
+  apply A.eq_trans with (fst z). auto. auto with ordered_type.
   generalize (@A.lt_not_eq (fst z) (fst y)); intro.
   elim H5. apply A.lt_trans with (fst x); auto.
   apply A.eq_sym; auto.
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index b9300fd7..4fb38ff8 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -864,7 +864,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pisel rd r1 r2 bit =>
       let v :=
           match rs#(reg_of_crbit bit) with
-          | Vint n => if Int.eq n Int.zero then rs#r2 else rs#r1
+          | Vint n => if Int.eq n Int.zero then rs#r2 else (gpr_or_zero rs r1)
           | _ => Vundef
           end in
       Next (nextinstr (rs #rd <- v #GPR0 <- Vundef)) m
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 884d5366..20cf9c1d 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1284,7 +1284,9 @@ Proof.
       reflexivity.
     + Simpl.
       rewrite <- (C r1), <- (C r2) by auto.
-      rewrite B. destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize.
+      rewrite B, gpr_or_zero_not_zero.
+      destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize.
+      destruct dir; intros e; subst; discriminate.
     + intros. Simpl.
 Qed.
 
diff --git a/test/clightgen/issue319.c b/test/clightgen/issue319.c
new file mode 100644
index 00000000..be9f3f7e
--- /dev/null
+++ b/test/clightgen/issue319.c
@@ -0,0 +1,12 @@
+/* Dollar signs in identifiers */
+
+int c$d = 42;
+
+int a$b(int x$$) {
+  return c$d + x$$;
+}
+
+int main(int argc, const char *argv[])
+{
+  return a$b(6);
+}