Merge branch 'master' of github.com:AbsInt/CompCert

11 files changed, 83 insertions, 24 deletions

diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index 75724d43..bb0c0c04 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(* Simple functions to serialize powerpc Asm to JSON *)
+(* Simple functions to serialize arm Asm to JSON *)
 
 (* Dummy function *)
 
diff --git a/backend/Fileinfo.ml b/backend/Fileinfo.ml
index afdea382..0490def0 100644
--- a/backend/Fileinfo.ml
+++ b/backend/Fileinfo.ml
@@ -42,16 +42,17 @@ let enter_filename f =
 
 (* Add file and line debug location, using GNU assembler-style DWARF2
    directives *)
+let print_file oc file =
+  try
+    Hashtbl.find filename_info file
+  with Not_found ->
+    let (filenum, filebuf as res) = enter_filename file in
+    fprintf oc "	.file	%d %S\n" filenum file;
+    res
 
 let print_file_line oc pref file line =
   if !Clflags.option_g && file <> "" then begin
-    let (filenum, filebuf) =
-      try
-        Hashtbl.find filename_info file
-      with Not_found ->
-        let (filenum, filebuf as res) = enter_filename file in
-        fprintf oc "	.file	%d %S\n" filenum file;
-        res in
+    let (filenum, filebuf) = print_file oc file in
     fprintf oc "	.loc	%d %d\n" filenum line;
     match filebuf with
     | None -> ()
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 90bbfe5a..0def347f 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -273,6 +273,42 @@ let combine_types mode env t1 t2 =
 
   in try Some(comp mode t1 t2) with Incompat -> None
 
+let rec equal_types env t1 t2 =
+  match t1, t2 with
+  | TVoid a1, TVoid a2 ->
+     a1=a2
+  | TInt(ik1, a1), TInt(ik2, a2) ->
+      ik1 = ik2 && a1 = a2
+  | TFloat(fk1, a1), TFloat(fk2, a2) ->
+     fk1 = fk2 && a1 = a2
+  | TPtr(ty1, a1), TPtr(ty2, a2) ->
+      a1 = a2 && equal_types env ty1 ty2
+  | TArray(ty1, sz1, a1), TArray(ty2, sz2, a2) ->
+      let size = begin match sz1,sz2 with
+      | None, None -> true
+      | Some s1, Some s2 -> s1 = s2
+      | _ -> false end in
+      size && a1 = a2 && equal_types env t1 t2
+  | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) ->
+      let params =
+        match params1, params2 with
+        | None, None -> true
+        | None, Some _
+        | Some _, None -> false
+        | Some l1, Some l2 ->
+            try
+              List.for_all2 (fun (_,t1) (_,t2) -> equal_types env t1 t2) l1 l2
+            with _ -> false
+      in params && a1 = a2 && vararg1 = vararg2 && equal_types env ty1 ty2
+  | TNamed _, _ -> equal_types env (unroll env t1) t2
+  | _, TNamed _ -> equal_types env t1 (unroll env t2)
+  | TStruct(s1, a1), TStruct(s2, a2)
+  | TUnion(s1, a1), TUnion(s2, a2)
+  | TEnum(s1, a1), TEnum(s2, a2) ->
+      s1 = s2 && a1 = a2
+  | _, _ ->
+      false
+
 (** Check whether two types are compatible. *)
 
 let compatible_types mode env t1 t2 =
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index b9879339..a322bfb1 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -80,6 +80,8 @@ val combine_types : attr_handling -> Env.t -> typ -> typ -> typ option
      with the same meaning as for [compatible_types].
      When two sets of attributes are compatible, the result of
      [combine_types] carries the union of these two sets of attributes. *)
+val equal_types : Env.t -> typ -> typ -> bool
+   (* Check that the two given types are equal up to typedef use *)
 
 (* Size and alignment *)
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index e81e6139..d1dce41f 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1786,13 +1786,21 @@ let enter_typedefs loc env sto dl =
   List.fold_left (fun env (s, ty, init) ->
     if init <> NO_INIT then
       error loc "initializer in typedef";
-    if redef Env.lookup_typedef env s then
-      error loc "redefinition of typedef '%s'" s;
-    if redef Env.lookup_ident env s then
-      error loc "redefinition of identifier '%s' as different kind of symbol" s;
-    let (id, env') = Env.enter_typedef env s ty in
-    emit_elab env loc (Gtypedef(id, ty));
-    env') env dl
+    match previous_def Env.lookup_typedef env s with
+    | Some (s',ty') ->
+        if equal_types env ty ty' then begin
+          warning loc "redefinition of typedef '%s'" s;
+          env
+        end else begin
+          error loc "redefinition of typedef '%s' with different type" s;
+          env
+        end
+    | None ->
+        if redef Env.lookup_ident env s then
+          error loc "redefinition of identifier '%s' as different kind of symbol" s;
+        let (id, env') = Env.enter_typedef env s ty in
+        emit_elab env loc (Gtypedef(id, ty));
+        env') env dl
 
 let enter_or_refine_ident local loc env s sto ty =
   if redef Env.lookup_typedef env s then
diff --git a/debug/Debug.ml b/debug/Debug.ml
index 348310f6..161ee3ed 100644
--- a/debug/Debug.ml
+++ b/debug/Debug.ml
@@ -47,7 +47,8 @@ type implem =
      mutable atom_parameter: ident -> ident -> atom -> unit;
      mutable add_compilation_section_start: string -> int -> unit;
      mutable add_compilation_section_end: string -> int -> unit;
-     mutable compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit;
+     mutable compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit;
+     mutable compute_gnu_file_enum: (string -> unit) -> unit;
      mutable exists_section: string -> bool;
      mutable remove_unused: ident -> unit;
      mutable variable_printed: string -> unit;
@@ -81,7 +82,8 @@ let implem =
    atom_parameter = (fun _ _ _ -> ());
    add_compilation_section_start = (fun _ _ -> ());
    add_compilation_section_end = (fun _ _ -> ());
-   compute_file_enum = (fun _ _ _ -> ());
+   compute_diab_file_enum = (fun _ _ _ -> ());
+   compute_gnu_file_enum = (fun _ -> ());
    exists_section = (fun _ -> true);
    remove_unused = (fun _ -> ());
    variable_printed = (fun _ -> ());
@@ -114,7 +116,8 @@ let atom_parameter fid pid atom = implem.atom_parameter fid pid atom
 let add_compilation_section_start sec addr = implem.add_compilation_section_start sec addr
 let add_compilation_section_end sec addr = implem.add_compilation_section_end sec addr
 let exists_section sec = implem.exists_section sec
-let compute_file_enum end_l entry_l line_e = implem.compute_file_enum end_l entry_l line_e
+let compute_diab_file_enum end_l entry_l line_e = implem.compute_diab_file_enum end_l entry_l line_e
+let compute_gnu_file_enum f = implem.compute_gnu_file_enum f
 let remove_unused ident = implem.remove_unused ident
 let variable_printed ident = implem.variable_printed ident
 let add_diab_info sec addr = implem.add_diab_info sec addr
diff --git a/debug/Debug.mli b/debug/Debug.mli
index 98a13b30..577b0ef8 100644
--- a/debug/Debug.mli
+++ b/debug/Debug.mli
@@ -45,7 +45,8 @@ type implem =
      mutable atom_parameter: ident -> ident -> atom -> unit;
      mutable add_compilation_section_start: string -> int -> unit;
      mutable add_compilation_section_end: string -> int -> unit;
-     mutable compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit;
+     mutable compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit;
+     mutable compute_gnu_file_enum: (string -> unit) -> unit;
      mutable exists_section: string -> bool;
      mutable remove_unused: ident -> unit;
      mutable variable_printed: string -> unit;
@@ -79,7 +80,8 @@ val generate_debug_info: (atom -> string) -> string -> debug_entries option
 val atom_parameter: ident -> ident -> atom -> unit
 val add_compilation_section_start: string -> int -> unit
 val add_compilation_section_end: string -> int -> unit
-val compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit
+val compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit
+val compute_gnu_file_enum: (string -> unit) -> unit
 val exists_section: string -> bool
 val remove_unused: ident -> unit
 val variable_printed: string -> unit
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 36138882..874dfb77 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -663,7 +663,7 @@ let exists_section sec =
 
 let filenum: (string * string,int) Hashtbl.t = Hashtbl.create 7
 
-let compute_file_enum end_label entry_label line_end =
+let compute_diab_file_enum end_label entry_label line_end =
   Hashtbl.iter (fun sec (_,_,secname) ->
     Hashtbl.add compilation_section_end sec (end_label secname);
     StringSet.iter (fun file ->
@@ -671,6 +671,9 @@ let compute_file_enum end_label entry_label line_end =
       Hashtbl.add filenum (sec,file) lbl) !all_files;
     line_end ()) diab_additional
 
+let compute_gnu_file_enum f =
+  StringSet.iter f !all_files
+
 let printed_vars: StringSet.t ref = ref StringSet.empty
 
 let variable_printed id =
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml
index 5aac6566..7ee56ff1 100644
--- a/debug/DebugInit.ml
+++ b/debug/DebugInit.ml
@@ -48,7 +48,8 @@ let init_debug () =
   implem.atom_parameter <- DebugInformation.atom_parameter;
   implem.add_compilation_section_start <- DebugInformation.add_compilation_section_start;
   implem.add_compilation_section_end <- DebugInformation.add_compilation_section_end;
-  implem.compute_file_enum <- DebugInformation.compute_file_enum;
+  implem.compute_diab_file_enum <- DebugInformation.compute_diab_file_enum;
+  implem.compute_gnu_file_enum <- DebugInformation.compute_gnu_file_enum;
   implem.exists_section <- DebugInformation.exists_section;
   implem.remove_unused <- DebugInformation.remove_unused;
   implem.variable_printed <- DebugInformation.variable_printed;
@@ -80,6 +81,8 @@ let init_none () =
   implem.atom_parameter <- (fun _ _ _ -> ());
   implem.add_compilation_section_start <- (fun _ _ -> ());
   implem.add_compilation_section_end <- (fun _ _ -> ());
+  implem.compute_diab_file_enum <- (fun _ _ _ -> ());
+  implem.compute_gnu_file_enum <- (fun _ -> ());
   implem.exists_section <- (fun _ -> true);
   implem.remove_unused <- (fun _ -> ());
   implem.variable_printed <- (fun _ -> ());
diff --git a/ia32/AsmToJSON.ml b/ia32/AsmToJSON.ml
index de39cb9d..3214491f 100644
--- a/ia32/AsmToJSON.ml
+++ b/ia32/AsmToJSON.ml
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(* Simple functions to serialize powerpc Asm to JSON *)
+(* Simple functions to serialize ia32 Asm to JSON *)
 
 (* Dummy function *)
 let p_program oc prog =
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 579573b9..530e269d 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -161,6 +161,7 @@ module Linux_System : SYSTEM =
         begin
           let high_pc = new_label () in
           Debug.add_compilation_section_end ".text" high_pc;
+          Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
           section oc Section_text;
           fprintf oc "%a:\n" label high_pc
         end
@@ -286,7 +287,7 @@ module Diab_System : SYSTEM =
         fprintf oc ".L%d:	.d2filenum \"%s\"\n" label f;
         label
       and end_line () =   fprintf oc "	.d2_line_end\n" in
-      Debug.compute_file_enum end_label entry_label end_line
+      Debug.compute_diab_file_enum end_label entry_label end_line
 
   end