Improved handling of C90 calls to undeclared functions

In a call such as "f(expr, ..., expr)", if the identifier "f" is not declared, declare it as specified in the ISO C90 standard, namely like "extern int f()" would do it.  Previously, the declaration was done "on the side" and not properly recorded in the environments.

The diff is relatively large because the "enter_or_refine_ident" had to be moved up in the file.

1 files changed, 75 insertions, 73 deletions

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 8c90bbc8..1888f053 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -107,6 +107,77 @@ let redef fn env arg =
   | None -> false
   | Some(id, info) -> Env.in_current_scope env id
 
+(* Auxiliaries for handling declarations and redeclarations *)
+
+let combine_toplevel_definitions loc env s old_sto old_ty sto ty =
+  let new_ty =
+    match combine_types AttrCompat env old_ty ty with
+    | Some new_ty ->
+        new_ty
+    | None ->
+        error loc
+           "redefinition of '%s' with incompatible type.@ \
+            Previous type: %a.@ \
+            New type: %a"
+          s Cprint.typ old_ty Cprint.typ ty;
+        ty in
+  let new_sto =
+    (* The only case not allowed is removing static *)
+    match old_sto,sto with
+    | Storage_static,Storage_static
+    | Storage_extern,Storage_extern
+    | Storage_register,Storage_register
+    | Storage_default,Storage_default -> sto
+    | _,Storage_static ->
+       error loc "static redefinition of '%s' after non-static definition" s;
+       sto
+    | Storage_static,_ -> Storage_static (* Static stays static *)
+    | Storage_extern,_ -> sto
+    | Storage_default,Storage_extern -> Storage_extern
+    | _,Storage_extern -> old_sto
+    | _,Storage_register
+    | Storage_register,_ -> Storage_register
+  in
+    (new_sto, new_ty)
+
+let enter_or_refine_ident local loc env s sto ty =
+  (* Check for illegal redefinitions:
+       - a name that was previously a typedef
+       - a variable that was already declared in the same local scope
+         (unless both old and new declarations are extern)
+       - an enum that was already declared in the same scope.
+     Redefinition of a variable at global scope (or extern) is treated below. *)
+  if redef Env.lookup_typedef env s then
+    error loc "redefinition of typedef '%s' as different kind of symbol" s;
+  begin match previous_def Env.lookup_ident env s with
+  | Some(id, II_ident(old_sto, old_ty))
+    when local && Env.in_current_scope env id
+               && not (sto = Storage_extern && old_sto = Storage_extern) ->
+      error loc "redefinition of local variable '%s'" s
+  | Some(id, II_enum _) when Env.in_current_scope env id ->
+     error loc "redefinition of enumerator '%s'" s
+  | _ ->
+     ()
+  end;
+  (* For a block-scoped, non-"extern" variable, a new declaration
+     is entered, and it has no linkage. *)
+  if local && sto <> Storage_extern then begin
+    let (id, env') = Env.enter_ident env s sto ty in
+    (id, sto, env', ty, false)
+  end else begin
+  (* For a file-scoped or "extern" variable, we need to check against
+     prior declarations of this variable with internal or external linkage.
+     The variable has linkage. *)
+    match previous_def Env.lookup_ident !top_environment s with
+    | Some(id, II_ident(old_sto, old_ty)) ->
+        let (new_sto, new_ty) =
+          combine_toplevel_definitions loc env s old_sto old_ty sto ty in
+        (id, new_sto, Env.add_ident env id new_sto new_ty, new_ty, true)
+    | _ ->
+        let (id, env') = Env.enter_ident env s sto ty in
+        (id, sto, env', ty, true)
+  end
+
 (* Forward declarations *)
 
 let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp * Env.t) ref
@@ -1353,11 +1424,11 @@ let elab_expr loc env a =
         | VARIABLE n when not (Env.ident_is_bound env n) ->
             warning "implicit declaration of function '%s'" n;
             let ty = TFun(TInt(IInt, []), None, false, []) in
+            (* Check against other definitions and enter in env *)
+            let (id, sto, env, ty, linkage) =
+              enter_or_refine_ident true loc env n Storage_extern ty in
             (* Emit an extern declaration for it *)
-            (* FIXME: could conflict with an earlier extern declaration
-               that is not in scope.  *)
-            let id = Env.fresh_ident n in
-            emit_elab env loc (Gdecl(Storage_extern, id, ty, None));
+            emit_elab ~linkage env loc (Gdecl(sto, id, ty, None));
             { edesc = EVar id; etyp = ty },env
         | _ -> elab env a1 in
       let bl = mmap  elab env al in
@@ -1847,75 +1918,6 @@ let enter_typedefs loc env sto dl =
         emit_elab env loc (Gtypedef(id, ty));
         env') env dl
 
-let combine_toplevel_definitions loc env s old_sto old_ty sto ty =
-  let new_ty =
-    match combine_types AttrCompat env old_ty ty with
-    | Some new_ty ->
-        new_ty
-    | None ->
-        error loc
-           "redefinition of '%s' with incompatible type.@ \
-            Previous type: %a.@ \
-            New type: %a"
-          s Cprint.typ old_ty Cprint.typ ty;
-        ty in
-  let new_sto =
-    (* The only case not allowed is removing static *)
-    match old_sto,sto with
-    | Storage_static,Storage_static
-    | Storage_extern,Storage_extern
-    | Storage_register,Storage_register
-    | Storage_default,Storage_default -> sto
-    | _,Storage_static ->
-       error loc "static redefinition of '%s' after non-static definition" s;
-       sto
-    | Storage_static,_ -> Storage_static (* Static stays static *)
-    | Storage_extern,_ -> sto
-    | Storage_default,Storage_extern -> Storage_extern
-    | _,Storage_extern -> old_sto
-    | _,Storage_register
-    | Storage_register,_ -> Storage_register
-  in
-    (new_sto, new_ty)
-
-let enter_or_refine_ident local loc env s sto ty =
-  (* Check for illegal redefinitions:
-       - a name that was previously a typedef
-       - a variable that was already declared in the same local scope
-         (unless both old and new declarations are extern)
-       - an enum that was already declared in the same scope.
-     Redefinition of a variable at global scope (or extern) is treated below. *)
-  if redef Env.lookup_typedef env s then
-    error loc "redefinition of typedef '%s' as different kind of symbol" s;
-  begin match previous_def Env.lookup_ident env s with
-  | Some(id, II_ident(old_sto, old_ty))
-    when local && Env.in_current_scope env id
-               && not (sto = Storage_extern && old_sto = Storage_extern) ->
-      error loc "redefinition of local variable '%s'" s
-  | Some(id, II_enum _) when Env.in_current_scope env id ->
-     error loc "redefinition of enumerator '%s'" s
-  | _ ->
-     ()
-  end;
-  (* For a block-scoped, non-"extern" variable, a new declaration
-     is entered, and it has no linkage. *)
-  if local && sto <> Storage_extern then begin
-    let (id, env') = Env.enter_ident env s sto ty in
-    (id, sto, env', ty, false)
-  end else begin
-  (* For a file-scoped or "extern" variable, we need to check against
-     prior declarations of this variable with internal or external linkage.
-     The variable has linkage. *)
-    match previous_def Env.lookup_ident !top_environment s with
-    | Some(id, II_ident(old_sto, old_ty)) ->
-        let (new_sto, new_ty) =
-          combine_toplevel_definitions loc env s old_sto old_ty sto ty in
-        (id, new_sto, Env.add_ident env id new_sto new_ty, new_ty, true)
-    | _ ->
-        let (id, env') = Env.enter_ident env s sto ty in
-        (id, sto, env', ty, true)
-  end
-
 let enter_decdefs local loc env sto dl =
   (* Sanity checks on storage class *)
   if sto = Storage_register && not local then