CBMC C++ frontend doesn't support namespace attributes

[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.

[tautschnig]

I'd much encourage you to create a PR with exactly this patch! The current C++ front-end is in a best-effort state, so we'll notice when we need more than the above patch when new tests come up!

[smowton]

#2360

[smowton]

The C++ standard one is trickier -- want to always pass -std=c++03 to the preprocessor if we're not told otherwise?

[tautschnig]

Really #2360 (Java instanceof)?

[tautschnig]

Yes, we should always pass some -std - I'm however leaning towards -std=c++98.

[smowton]

Oops. #2362

[tautschnig]

Fixed via #2362.