diff --git a/regression/Makefile b/regression/Makefile index ba29a2d779..7f7c15c584 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -25,6 +25,7 @@ DIRS = cbmc \ goto-cc-goto-analyzer \ systemc \ contracts \ + goto-cc-file-local \ # Empty last line # Run all test directories in sequence diff --git a/regression/goto-cc-file-local/Makefile b/regression/goto-cc-file-local/Makefile new file mode 100644 index 0000000000..504a174cd8 --- /dev/null +++ b/regression/goto-cc-file-local/Makefile @@ -0,0 +1,35 @@ +default: tests.log + +include ../../src/config.inc +include ../../src/common + +ifeq ($(BUILD_ENV_),MSVC) + exe=../../../src/goto-cc/goto-cl + is_windows=true +else + exe=../../../src/goto-cc/goto-cc + is_windows=false +endif + +test: + @../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' + +tests.log: + @../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + @for dir in *; do \ + $(RM) tests.log; \ + if [ -d "$$dir" ]; then \ + cd "$$dir"; \ + $(RM) *.out *.gb; \ + cd ..; \ + fi \ + done diff --git a/regression/goto-cc-file-local/chain.sh b/regression/goto-cc-file-local/chain.sh index 168a75a2ab..557e185673 100755 --- a/regression/goto-cc-file-local/chain.sh +++ b/regression/goto-cc-file-local/chain.sh @@ -4,6 +4,8 @@ # # Author: Kareem Khazem +set -e + is_in() { [[ "$2" =~ $1 ]] && return 0 || return 1 @@ -81,6 +83,7 @@ done if is_in final-link "$ALL_ARGS"; then OUT_FILE=final-link.gb + rm -f ${OUT_FILE} if [[ "${is_windows}" == "true" ]]; then "${goto_cc}" \ --export-function-local-symbols \ diff --git a/regression/goto-cc-file-local/function-pointer/main.c b/regression/goto-cc-file-local/function-pointer/main.c new file mode 100644 index 0000000000..bb2caa8c86 --- /dev/null +++ b/regression/goto-cc-file-local/function-pointer/main.c @@ -0,0 +1,14 @@ +#include + +static int foo() +{ + return 3; +} + +int (*fptrs[])(void) = {foo}; + +int main() +{ + int x = fptrs[0](); + assert(x == 3); +} diff --git a/regression/goto-cc-file-local/function-pointer/test.desc b/regression/goto-cc-file-local/function-pointer/test.desc new file mode 100644 index 0000000000..bcb680f7f7 --- /dev/null +++ b/regression/goto-cc-file-local/function-pointer/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +final-link assertion-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^\*\*\*\* WARNING: no body for function diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h index a4a5beaa35..89eda1e411 100644 --- a/src/goto-programs/name_mangler.h +++ b/src/goto-programs/name_mangler.h @@ -84,6 +84,20 @@ public: for(const auto &sym : old_syms) model.symbol_table.erase(sym); + for(const auto &sym_pair : model.symbol_table) + { + const symbolt &sym = sym_pair.second; + + exprt e = sym.value; + typet t = sym.type; + if(rename(e) && rename(t)) + continue; + + symbolt &new_sym = model.symbol_table.get_writeable_ref(sym.name); + new_sym.value = e; + new_sym.type = t; + } + for(auto &fun : model.goto_functions.function_map) { if(!fun.second.body_available()) diff --git a/src/util/rename_symbol.h b/src/util/rename_symbol.h index 466e649c3c..8fcd4538cb 100644 --- a/src/util/rename_symbol.h +++ b/src/util/rename_symbol.h @@ -43,14 +43,18 @@ public: type_map.insert(std::pair(old_id, new_id)); } - void operator()(exprt &dest) const + /// Rename symbols in \p dest. + /// \return True if, and only if, the expression was not modified. + bool operator()(exprt &dest) const { - rename(dest); + return rename(dest); } - void operator()(typet &dest) const + /// Rename symbols in \p dest. + /// \return True if, and only if, the type was not modified. + bool operator()(typet &dest) const { - rename(dest); + return rename(dest); } rename_symbolt();