C front-end: Record extern declarations in current scope

[tautschnig]

Previously, extern declarations would only be recorded in the global scope.
While they do belong to the global scope, they still need to take precedence in
name lookups in the local/current scope as well.

Also removing an unnecessary iostream include.

Fixes: #1867

[martin-cs]

Looks like it could fix the issue (given my understanding of the front-end ...). I'm not sure it captures all of the rules described in the C standard. Maybe, depending on what @hannes-steffenhagen-diffblue wanted from / for the original issue he might be able / willing / interested / motivated / inclined to write additional test cases which cover the rules more fully.

[hannes-steffenhagen-diffblue]

Good catch

[tautschnig]

@hannes-steffenhagen-diffblue Just let us know whether you would be willing/able to provide more tests. Else I'll merge as soon as @kroening approves.

[hannes-steffenhagen-diffblue]

This fixes the issue in the case of a local variable; Unfortunately it doesn't work with parameters, consider

int param;
void function(int param)
{
  printf("%d\n", param);
  {
    extern int param;
    printf("%d\n", param);
  }
}

int main(void)
{
  param = 2;
  function(1);
}

Function parameters have block scope, just like local variables, see 6.2.1.4:

Every other identifier has scope determined by the placement of its declaration (in a
declarator or type specifier). If the declarator or type specifier that declares the identifier
appears outside of any block or list of parameters, the identifier has file scope, which
terminates at the end of the translation unit. If the declarator or type specifier that
declares the identifier appears inside a block or within the list of parameter declarations in
a function definition, the identifier has block scope, which terminates at the end of the
associated block. If the declarator or type specifier that declares the identifier appears within the list of parameter declarations in a function prototype (not part of a function
definition), the identifier has function prototype scope, which terminates at the end of the
function declarator. If an identifier designates two different entities in the same name
space, the scopes might overlap. If so, the scope of one entity (the inner scope) will be a
strict subset of the scope of the other entity (the outer scope). Within the inner scope, the
identifier designates the entity declared in the inner scope; the entity declared in the outer
scope is hidden (and not visible) within the inner scope.

To do this, function parameter names would have to be rewritten similarly to how local variables currently are (since the have the same scope as top level local variables anyway, they could be rewritten to function_name$$1$$arg_name just like those are. Would that be reasonable @martin-cs ?

[tautschnig]

This fixes the issue in the case of a local variable; Unfortunately it doesn't work with parameters, consider [...]

Are you sure this is actually broken? CBMC verifies the following very much correctly:

#include <stdio.h>
#include <assert.h>

int param;
void function(int param)
{
  printf("%d\n", param);
  {
    extern int param;
    printf("%d\n", param);
    assert(param == 2);
  }
  assert(param == 1);
}

int main(void)
{
  param = 2;
  function(1);
}

To do this, function parameter names would have to be rewritten similarly to how local variables currently are (since the have the same scope as top level local variables anyway, they could be rewritten to function_name$$1$$arg_name just like those are.

Function parameters are rewritten to function_name::arg_name, but indeed at least dump-c is broken for this example.

[hannes-steffenhagen-diffblue]

Ah, you're right, verification does indeed work correctly. I was going off the output of goto-instrument --show-goto-functions, which is incorrect, as is goto-instrument --dump-c. I'm less concerned about that than I am about the verification working, so I'd consider that a different bug to what this is fixing.

[tautschnig]

I have no added the parameter-based test that @hannes-steffenhagen-diffblue proposed and have included a fix that addresses the problems in the output of show-goto-functions or dump-c.

[tautschnig]

I'm not sure what this AppVeyor failure is; I'll wait for Travis to finish to see whether it can give me more clues. (I can't reproduce it locally at the moment.)

[tautschnig]

@karkhaz, everyone: This PR now includes the bugfix 3602d21 - it should possibly be migrated into its own PR, but it's really here where the problems showed up (on regression/cbmc/coverage_report1).

[kroening]

This one is straight forward, but I am still puzzled by 3602d21.

[tautschnig]

@kroening: what is it that's puzzling? My commit message likely isn't good enough. For a start: the culprit is line 195 of symex_main.cpp, which sets up the eventually broken namespace.

[kroening]

The next thing that irritates me there is the copy made of the new symbols:
// Clients may need to construct a namespace with both the names in
// the original goto-program and the names generated during symbolic
// execution, so return the names generated through symbolic execution
// through new_symbol_table.
new_symbol_table = state.symbol_table;

[kroening]

I would say the whole way symbol tables are handled there needs a full re-think.