C++ front-end: Declarator to symbol conversion follows C implementation [depends-on: #4559]

regression/cbmc-cpp/CMakeLists.txt

@@ -1,3 +1,9 @@
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>" -X gcc-only
+)
+else()
 add_test_pl_tests(
     "$<TARGET_FILE:cbmc>"
 )
+endif()

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 \

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
+}

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$

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 \

src/cpp/cpp_declarator.h

@@ -45,6 +45,16 @@ class cpp_declaratort:public exprt
     return static_cast<const exprt &>(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()
   {

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)

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();
+}

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 <util/source_location.h>
+#include <util/type.h>
 
 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<source_locationt &>(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

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);