diff options
-rw-r--r-- | cparser/Elab.ml | 148 |
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 |