From 87c5948ef6da9c9d577933ff07677d0a684489f3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 21 Feb 2018 08:59:18 +0000 Subject: [PATCH 1/2] C front-end: Record extern declarations in current scope 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 --- regression/cbmc/extern1/main.c | 31 +++++++++++++++++++++++++++++++ regression/cbmc/extern1/test.desc | 7 +++++++ regression/cbmc/extern2/main.c | 20 ++++++++++++++++++++ regression/cbmc/extern2/test.desc | 7 +++++++ src/ansi-c/ansi_c_parser.cpp | 7 +++---- 5 files changed, 68 insertions(+), 4 deletions(-) create mode 100644 regression/cbmc/extern1/main.c create mode 100644 regression/cbmc/extern1/test.desc create mode 100644 regression/cbmc/extern2/main.c create mode 100644 regression/cbmc/extern2/test.desc diff --git a/regression/cbmc/extern1/main.c b/regression/cbmc/extern1/main.c new file mode 100644 index 00000000000..73a25e3a034 --- /dev/null +++ b/regression/cbmc/extern1/main.c @@ -0,0 +1,31 @@ +#include +#include + +int some_global = 10; + +void shadow() +{ + int some_global = 5; + + printf("local: %d\n", some_global); + { + int some_global = 0; + ++some_global; + printf("local2: %d\n", some_global); + } + + printf("local: %d\n", some_global); + { + extern int some_global; + ++some_global; + printf("global: %d\n", some_global); + assert(some_global == 11); + } + + assert(some_global == 5); +} + +int main(void) +{ + shadow(); +} diff --git a/regression/cbmc/extern1/test.desc b/regression/cbmc/extern1/test.desc new file mode 100644 index 00000000000..9c96469df12 --- /dev/null +++ b/regression/cbmc/extern1/test.desc @@ -0,0 +1,7 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/cbmc/extern2/main.c b/regression/cbmc/extern2/main.c new file mode 100644 index 00000000000..0fe1322da5e --- /dev/null +++ b/regression/cbmc/extern2/main.c @@ -0,0 +1,20 @@ +#include +#include + +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); +} diff --git a/regression/cbmc/extern2/test.desc b/regression/cbmc/extern2/test.desc new file mode 100644 index 00000000000..9c96469df12 --- /dev/null +++ b/regression/cbmc/extern2/test.desc @@ -0,0 +1,7 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp index 46d9f51d1b4..7957b9fdd87 100644 --- a/src/ansi-c/ansi_c_parser.cpp +++ b/src/ansi-c/ansi_c_parser.cpp @@ -8,8 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_parser.h" -#include - #include "c_storage_spec.h" ansi_c_parsert ansi_c_parser; @@ -35,8 +33,6 @@ ansi_c_id_classt ansi_c_parsert::lookup( if(n_it!=it->name_map.end()) { - assert(id2string(n_it->second.prefixed_name)== - it->prefix+id2string(scope_name)); identifier=n_it->second.prefixed_name; return n_it->second.id_class; } @@ -150,6 +146,9 @@ void ansi_c_parsert::add_declarator( ansi_c_identifiert &identifier=scope.name_map[base_name]; identifier.id_class=id_class; identifier.prefixed_name=prefixed_name; + + if(force_root_scope) + current_scope().name_map[base_name] = identifier; } ansi_c_declaration.declarators().push_back(new_declarator); From e276b271bfc7319a46043f4fbc798f2404162698 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 21 Feb 2018 15:29:22 +0000 Subject: [PATCH 2/2] Avoid extern/parameter name collisions in show-goto-functions/dump-c output While the preceding patch in this series ensures that the internal representation is consistent, plain-text output would still have collisions between parameter names and globals declared extern, because parameters were never renamed. We now detect conflicts between prettified names and global variable names. Also added a comment explaining a somewhat obscure bit of code. --- src/ansi-c/expr2c.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 215f05d39bd..259a6bfe2e4 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -89,7 +89,7 @@ void expr2ct::get_shorthands(const exprt &expr) find_symbols_sett symbols; find_symbols(expr, symbols); - // avoid renaming parameters + // avoid renaming parameters, if possible for(find_symbols_sett::const_iterator it=symbols.begin(); it!=symbols.end(); @@ -103,7 +103,16 @@ void expr2ct::get_shorthands(const exprt &expr) irep_idt sh=id_shorthand(*it); - ns_collision[symbol->location.get_function()].insert(sh); + std::string func = id2string(*it); + func = func.substr(0, func.rfind("::")); + + // if there is a global symbol of the same name as the shorthand (even if + // not present in this particular expression) then there is a collision + const symbolt *global_symbol; + if(!ns.lookup(sh, global_symbol)) + sh = func + "$$" + id2string(sh); + + ns_collision[func].insert(sh); if(!shorthands.insert(std::make_pair(*it, sh)).second) UNREACHABLE; @@ -125,6 +134,8 @@ void expr2ct::get_shorthands(const exprt &expr) if(!has_collision) { + // if there is a global symbol of the same name as the shorthand (even if + // not present in this particular expression) then there is a collision const symbolt *symbol; has_collision=!ns.lookup(sh, symbol); }