diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-06-04 16:31:12 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-04 16:31:12 +0200 |
| commit | 15d1bbdba079b2ff0778e6b0685338a0919f2aef (patch) | |
| tree | f9067d418f18e616472906a45e81a8b91d6d051f /cparser | |
| parent | 545df304d7c17acc475fb1b37f16959fcc430f6a (diff) | |
| download | compcert-kvx-15d1bbdba079b2ff0778e6b0685338a0919f2aef.tar.gz compcert-kvx-15d1bbdba079b2ff0778e6b0685338a0919f2aef.zip | |
Support redefinition of a typedef in another scope (#122)
The current check for redefinition is too strict, ruling out e.g.
```
typedef int t;
void f(void) { typedef char t; }
```
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 39b15279..b731245c 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2250,7 +2250,7 @@ let enter_typedefs loc env sto dl = if init <> NO_INIT then error loc "initializer in typedef"; match previous_def Env.lookup_typedef env s with - | Some (s',ty') -> + | Some (s',ty') when Env.in_current_scope env s' -> if equal_types env ty ty' then begin warning loc Celeven_extension "redefinition of typedef '%s' is C11 extension" s; env @@ -2259,7 +2259,7 @@ let enter_typedefs loc env sto dl = (print_typ env) ty (print_typ env) ty'; env end - | None -> + | _ -> if redef Env.lookup_ident env s then error loc "redefinition of '%s' as different kind of symbol" s; let (id, env') = Env.enter_typedef env s ty in |