diff --git a/regression/cbmc-cpp/CMakeLists.txt b/regression/cbmc-cpp/CMakeLists.txt index 93d5ee716c2..ea18a04ec8c 100644 --- a/regression/cbmc-cpp/CMakeLists.txt +++ b/regression/cbmc-cpp/CMakeLists.txt @@ -1,3 +1,9 @@ +if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") +add_test_pl_tests( + "$" -X gcc-only +) +else() add_test_pl_tests( "$" ) +endif() diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile index 4964810a03e..6601ae0d64a 100644 --- a/regression/cbmc-cpp/Makefile +++ b/regression/cbmc-cpp/Makefile @@ -1,10 +1,19 @@ default: tests.log +include ../../src/config.inc +include ../../src/common + +ifeq ($(BUILD_ENV_),MSVC) + gcc_only = -X gcc-only +else + gcc_only = +endif + test: - @../test.pl -e -p -c ../../../src/cbmc/cbmc + @../test.pl -e -p -c ../../../src/cbmc/cbmc $(gcc_only) tests.log: ../test.pl - @../test.pl -e -p -c ../../../src/cbmc/cbmc + @../test.pl -e -p -c ../../../src/cbmc/cbmc $(gcc_only) show: @for dir in *; do \ diff --git a/regression/cbmc-cpp/gcc_attributes1/main.cpp b/regression/cbmc-cpp/gcc_attributes1/main.cpp new file mode 100644 index 00000000000..6d7d6a83ce4 --- /dev/null +++ b/regression/cbmc-cpp/gcc_attributes1/main.cpp @@ -0,0 +1,12 @@ +#ifdef __GNUC__ +const char *__attribute__((weak)) bar(); +#endif + +int main() +{ +#ifdef __GNUC__ + return bar() != 0; +#else + return 0 +#endif +} diff --git a/regression/cbmc-cpp/gcc_attributes1/test.desc b/regression/cbmc-cpp/gcc_attributes1/test.desc new file mode 100644 index 00000000000..9ee17c5db09 --- /dev/null +++ b/regression/cbmc-cpp/gcc_attributes1/test.desc @@ -0,0 +1,10 @@ +CORE gcc-only +main.cpp +--show-symbol-table +activate-multi-line-match +Symbol\.+: bar\(\)\nPretty name\.+: bar\(\)\nModule\.+: main\nBase name\.+: bar\nMode\.+: cpp\nType\.+: auto \(\) -> const char \*\nValue\.+: \nFlags\.+: weak\n +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/cpp/Makefile b/src/cpp/Makefile index 3189c375ba7..fca6f614318 100644 --- a/src/cpp/Makefile +++ b/src/cpp/Makefile @@ -17,6 +17,7 @@ SRC = cpp_constructor.cpp \ cpp_parser.cpp \ cpp_scope.cpp \ cpp_scopes.cpp \ + cpp_storage_spec.cpp \ cpp_token_buffer.cpp \ cpp_type2name.cpp \ cpp_typecheck.cpp \ diff --git a/src/cpp/cpp_declarator.h b/src/cpp/cpp_declarator.h index d9cfbef296f..2f62817383a 100644 --- a/src/cpp/cpp_declarator.h +++ b/src/cpp/cpp_declarator.h @@ -45,6 +45,16 @@ class cpp_declaratort:public exprt return static_cast(find(ID_value)); } + bool get_is_parameter() const + { + return get_bool(ID_is_parameter); + } + + void set_is_parameter(bool is_parameter) + { + set(ID_is_parameter, is_parameter); + } + // initializers for function arguments exprt &init_args() { diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index cfe7910aebe..401c7e210ad 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -53,6 +53,9 @@ symbolt &cpp_declarator_convertert::convert( final_type=declarator.merge_type(declaration_type); assert(final_type.is_not_nil()); + cpp_storage_spect final_storage_spec = storage_spec; + final_storage_spec |= cpp_storage_spect(final_type); + cpp_template_args_non_tct template_args; // run resolver on scope @@ -135,7 +138,7 @@ symbolt &cpp_declarator_convertert::convert( if(!maybe_symbol && is_friend) { symbolt &friend_symbol = - convert_new_symbol(storage_spec, member_spec, declarator); + convert_new_symbol(final_storage_spec, member_spec, declarator); // mark it as weak so that the full declaration can replace the symbol friend_symbol.is_weak = true; return friend_symbol; @@ -191,7 +194,7 @@ symbolt &cpp_declarator_convertert::convert( type, declarator.member_initializers()); } - if(!storage_spec.is_extern()) + if(!final_storage_spec.is_extern()) symbol.is_extern=false; // initializer? @@ -217,10 +220,10 @@ symbolt &cpp_declarator_convertert::convert( const auto maybe_symbol= cpp_typecheck.symbol_table.get_writeable(final_identifier); if(!maybe_symbol) - return convert_new_symbol(storage_spec, member_spec, declarator); + return convert_new_symbol(final_storage_spec, member_spec, declarator); symbolt &symbol=*maybe_symbol; - if(!storage_spec.is_extern()) + if(!final_storage_spec.is_extern()) symbol.is_extern = false; if(declarator.get_bool(ID_C_template_case)) @@ -447,6 +450,9 @@ symbolt &cpp_declarator_convertert::convert_new_symbol( symbol.base_name=base_name; symbol.value=declarator.value(); symbol.location=declarator.name().source_location(); + symbol.is_extern = storage_spec.is_extern(); + symbol.is_parameter = declarator.get_is_parameter(); + symbol.is_weak = storage_spec.is_weak(); symbol.mode=linkage_spec==ID_auto?ID_cpp:linkage_spec; symbol.module=cpp_typecheck.module; symbol.type=final_type; @@ -459,49 +465,40 @@ symbolt &cpp_declarator_convertert::convert_new_symbol( symbol.value.is_not_nil()) symbol.is_macro=true; - if(member_spec.is_inline()) - to_code_type(symbol.type).set_inlined(true); - - if(!symbol.is_type) + if(is_code && !symbol.is_type) { - if(is_code) - { - // it is a function - if(storage_spec.is_static()) - symbol.is_file_local=true; - } - else - { - // it is a variable - symbol.is_state_var=true; - symbol.is_lvalue = !is_reference(symbol.type) && - !(symbol.type.get_bool(ID_C_constant) && - is_number(symbol.type) && - symbol.value.id() == ID_constant); - - if(cpp_typecheck.cpp_scopes.current_scope().is_global_scope()) - { - symbol.is_static_lifetime=true; + // it is a function + symbol.is_static_lifetime = false; + symbol.is_thread_local = false; - if(storage_spec.is_extern()) - symbol.is_extern=true; - } - else - { - if(storage_spec.is_static()) - { - symbol.is_static_lifetime=true; - symbol.is_file_local=true; - } - else if(storage_spec.is_extern()) - { - cpp_typecheck.error().source_location=storage_spec.location(); - cpp_typecheck.error() << "external storage not permitted here" - << messaget::eom; - throw 0; - } - } - } + symbol.is_file_local = storage_spec.is_static(); + + if(member_spec.is_inline()) + to_code_type(symbol.type).set_inlined(true); + } + else + { + symbol.is_lvalue = + !is_reference(symbol.type) && + !(symbol.type.get_bool(ID_C_constant) && is_number(symbol.type) && + symbol.value.id() == ID_constant); + + symbol.is_static_lifetime = + !symbol.is_macro && !symbol.is_type && + (cpp_typecheck.cpp_scopes.current_scope().is_global_scope() || + storage_spec.is_static()); + + symbol.is_thread_local = + (!symbol.is_static_lifetime && !storage_spec.is_extern()) || + storage_spec.is_thread_local(); + + symbol.is_file_local = + symbol.is_macro || + (!cpp_typecheck.cpp_scopes.current_scope().is_global_scope() && + !storage_spec.is_extern()) || + (cpp_typecheck.cpp_scopes.current_scope().is_global_scope() && + storage_spec.is_static()) || + symbol.is_parameter; } if(symbol.is_static_lifetime) diff --git a/src/cpp/cpp_storage_spec.cpp b/src/cpp/cpp_storage_spec.cpp new file mode 100644 index 00000000000..f0c15dc7a25 --- /dev/null +++ b/src/cpp/cpp_storage_spec.cpp @@ -0,0 +1,34 @@ +/*******************************************************************\ + +Module: + +Author: Michael Tautschnig + +\*******************************************************************/ + +#include "cpp_storage_spec.h" + +void cpp_storage_spect::read(const typet &type) +{ + if(type.id() == ID_merged_type || type.id() == ID_function_type) + { + forall_subtypes(it, type) + read(*it); + } + else if(type.id() == ID_static) + set_static(); + else if(type.id() == ID_extern) + set_extern(); + else if(type.id() == ID_auto) + set_auto(); + else if(type.id() == ID_register) + set_register(); + else if(type.id() == ID_mutable) + set_mutable(); + else if(type.id() == ID_thread_local) + set_thread_local(); + else if(type.id() == ID_asm) + set_asm(); + else if(type.id() == ID_weak) + set_weak(); +} diff --git a/src/cpp/cpp_storage_spec.h b/src/cpp/cpp_storage_spec.h index 74c11bc1ef0..255b6edf191 100644 --- a/src/cpp/cpp_storage_spec.h +++ b/src/cpp/cpp_storage_spec.h @@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #ifndef CPROVER_CPP_CPP_STORAGE_SPEC_H #define CPROVER_CPP_CPP_STORAGE_SPEC_H -#include +#include class cpp_storage_spect:public irept { @@ -19,6 +19,11 @@ class cpp_storage_spect:public irept { } + explicit cpp_storage_spect(const typet &type) + { + read(type); + } + source_locationt &location() { return static_cast(add(ID_C_source_location)); @@ -36,6 +41,10 @@ class cpp_storage_spect:public irept bool is_mutable() const { return get_bool(ID_mutable); } bool is_thread_local() const { return get_bool(ID_thread_local); } bool is_asm() const { return get_bool(ID_asm); } + bool is_weak() const + { + return get_bool(ID_weak); + } void set_static() { set(ID_static, true); } void set_extern() { set(ID_extern, true); } @@ -44,13 +53,41 @@ class cpp_storage_spect:public irept void set_mutable() { set(ID_mutable, true); } void set_thread_local() { set(ID_thread_local, true); } void set_asm() { set(ID_asm, true); } + void set_weak() + { + set(ID_weak, true); + } bool is_empty() const { - return !is_static() && !is_extern() && !is_auto() && - !is_register() && !is_mutable() && !is_thread_local() && - !is_asm(); + return !is_static() && !is_extern() && !is_auto() && !is_register() && + !is_mutable() && !is_thread_local() && !is_asm() && !is_weak(); + } + + cpp_storage_spect &operator|=(const cpp_storage_spect &other) + { + if(other.is_static()) + set_static(); + if(other.is_extern()) + set_extern(); + if(other.is_auto()) + set_auto(); + if(other.is_register()) + set_register(); + if(other.is_mutable()) + set_mutable(); + if(other.is_thread_local()) + set_thread_local(); + if(other.is_asm()) + set_asm(); + if(other.is_weak()) + set_weak(); + + return *this; } + +private: + void read(const typet &type); }; #endif // CPROVER_CPP_CPP_STORAGE_SPEC_H diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 351d7a82ee9..8c386779f12 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -4127,6 +4127,8 @@ bool Parser::rArgDeclaration(cpp_declarationt &declaration) if(!rDeclarator(arg_declarator, kArgDeclarator, true, false)) return false; + arg_declarator.set_is_parameter(true); + declaration.declarators().push_back(arg_declarator); int t=lex.LookAhead(0);