[C++ frontend] Consider handling the C++ standard while parsing the C++ libraries

[lucasccordeiro]

There are subtle differences in the C++ libraries between the different standards. See our discussion at https://github.com/esbmc/esbmc/pull/1675. We should consider handling the C++ standard while parsing the C++ libraries.

[XLiZHI]

This issue is not limited to the cpp standard, Perhaps we could consider standard library support as well.

The standard library is vast and constantly being updated and modified. It would be difficult and time-consuming to support all the standard libraries' funcions. I think the changes we can consider at the moment are:

1. For functions that cannot convert, instead of terminating ESBMC, we skip(hide) it.
2. Following a test-driven approach, we are gradually improving the frontend.

[fbrausse]

I am not entirely sure how to proceed with this issue. @lucasccordeiro is this only about the exception specifier on functions or did you intend it to cover a broader range of differences? In case of the latter, I think we should start compiling a list to get an overview of what's needed.

For the exception specifier: GCC has this in its \<bits/c++config.h>

// Macro for noexcept, to support in mixed 03/0x mode.
#ifndef _GLIBCXX_NOEXCEPT
# if __cplusplus >= 201103L
#  define _GLIBCXX_NOEXCEPT noexcept
#  define _GLIBCXX_NOEXCEPT_IF(...) noexcept(__VA_ARGS__)
#  define _GLIBCXX_USE_NOEXCEPT noexcept
#  define _GLIBCXX_THROW(_EXC)
# else
#  define _GLIBCXX_NOEXCEPT
#  define _GLIBCXX_NOEXCEPT_IF(...)
#  define _GLIBCXX_USE_NOEXCEPT throw()
#  define _GLIBCXX_THROW(_EXC) throw(_EXC)
# endif
#endif

We could consider putting something similar into our src/cpp/library/definitions.h (and potentially move that file into an ESBMC-specific sub-directory)

However, unless there are reports by users, I would suggest to not clutter our headers too much with these "quasi-optional" annotations in order to keep maintainability. While many of those annotations can indeed be checked with type trait templates and thereby influence how C++ user code is parsed, I think that it's not worth adding them proactively. Such checks seem to be rarely done outside of the standard library.