Revised handling of block-scoped extern declarations

Currently, CompCert incorrectly handles 'extern' and function
declarations within a block.  For example:

int main(void)
{
   {
        extern int i;
        i = 0;
   }
   {
        extern float i;
        i = 10;
   }
}

CompCert fails to detect the inconsistent declarations of "i" in the
two blocks, simply because the first declaration is not in scope when
the second declaration is processed.

This commit changes the elaboration of file-scope declarations,
block-scope "extern" declarations and block-scope function
declarations so that they are checked against possible earlier
declarations found in the already-elaborated top-level declarations,
instead of in the current typing environment.

Owing to the lifting of block-scoped extern and static declarations to
the top-level already performed by the elaboration pass, the
already-elaborated top-level declarations give an accurate view of the
declarations of variables with internal or external linkage already
encountered and processed, even if they are not currently in scope.

0 files changed, 0 insertions, 0 deletions