Parse error with gcc 6.3

[jamesjer]

WIth gcc 6.3, cbmc 5.6 fails one test, regression/cpp/enum8/test.desc, when processing this definition in /usr/include/c++/6.3.1/x86_64-redhat-linux/bits/c++config.h:

namespace std
{
  typedef __SIZE_TYPE__ 	size_t;
  typedef __PTRDIFF_TYPE__	ptrdiff_t;

#if __cplusplus >= 201103L
  typedef decltype(nullptr)	nullptr_t;
#endif
}

The issue arises from the nullptr_t definition, which cbmc's parser does not seem to understand. Running the test in c++98 mode works around the issue. However, on systems with gcc 6.3, runtime failures follow from the same issue; see https://bugzilla.redhat.com/show_bug.cgi?id=1414925 for one example.

[smowton]

Also fails:

int main(int argc, char** argv)
{

  int i = 3;
  decltype(i) j = 2;
  return i + j;

}

Replacing decltype with typeof circumvents the bug, so the fix shouldn't be too involved if we're happy with a 99% rather than a 100% faithful implementation of decltype's semantics.

[thomasspriggs]

The downstream redhat ticket reports that this issue was fixed in cbmc version 5.7. Therefore it would appear that this ticket is no longer needed. Please feel free to reopen if there are still problems related to this for us to resolve.