From 57fceab9ba11cb98635236f31c85ca976ca7f48c Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Sun, 4 Oct 2015 20:36:02 +0200
Subject: Allow redefinition of a typedef with the same name.

C11 allows a typedef redefinition if the types are the same.
We now allow this also and issue a warning and an error if the types are different.
---
 cparser/Cutil.ml  | 36 ++++++++++++++++++++++++++++++++++++
 cparser/Cutil.mli |  2 ++
 cparser/Elab.ml   | 22 +++++++++++++++-------
 3 files changed, 53 insertions(+), 7 deletions(-)

(limited to 'cparser')

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
-- 
cgit