Skip to content

CBMC C++ frontend doesn't support namespace attributes #2358

Closed
@smowton

Description

@smowton

Excerpt from glibc 2.27:

namespace std
{
  inline namespace __cxx11 __attribute__((__abi_tag__ ("cxx11"))) { }
}

The CBMC frontend however can't parse such a thing, as it doesn't expect attributes on namespaces. This causes tests that include <cassert> among other headers to fail.

A change such as the following successfully hacks around the problem:

--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -856,6 +856,16 @@ bool Parser::rNamespaceSpec(cpp_namespace_spect &namespace_spec)
   namespace_spec.set_namespace(name);
   namespace_spec.set_is_inline(is_inline);
 
+  if(lex.LookAhead(0)==TOK_GCC_ATTRIBUTE)
+  {
+    cpp_tokent tk;
+    lex.get_token(tk);
+
+    typet discard;
+    if(!rAttribute(discard))
+      return false;
+  }
+
   switch(lex.LookAhead(0))
   {
   case '{':

However I don't know enough about either the C++ grammar to say whether the attribute can occur in other places, or about the parser's structure to know whether a simple throw-away like that is sufficient.

Metadata

Metadata

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions