CBMC C++ frontend doesn't detect implicit -std option

[smowton]

With g++-7 at least, -std=c++14 is implied if the user doesn't make an explicit choice. However, cbmc's frontend expects c++03 unless something is explicitly specified. It should either check the __cplusplus defined by the compiler to find out what it understood to be the prevailing standard and act accordingly, or force -std=c++03. The former is better, as a configure script would be reasonable to avoid using -std if the compiler appears to be modern enough that it supports the desired language version without an explicit switch.

This causes all cpp regression tests that use decltype and similar to fail when the real compiler is g++7.

[smowton]

Suggestion: I think this series of problems with modern compilers indicates it's time we were CI'ing against multiple gcc versions.

[tautschnig]

At least for goto-cc that really just needs using the new gcc_version tool. I agree that CI'ing all this is desirable, likely that should be part of the same PR. Now let me just ask my time machine to get this implemented :-)

[tautschnig]

(But I'm accepting responsibility for eventually doing so.)

[smowton]

Gah, awkwardly the GCC default is actually -std=gnu++98 and -std=gnu++14 respectively, which compilers we merely think are GCC but which are actually something GCC-like are likely to choke on. I will therefore submit a patch using the gcc-version logic to choose.

[kroening]

Is this obsoleted by #2364?

[smowton]

That will fix it, if it works as I hope, yes.

[NlightNFotis]

@smowton Was this fixed by #2364 ? If yes can this be closed?

[sschwarzmann]

Maybe the errors I'm seeing fit in this issue report (resp. an update of the used branch deadlock-analysis with the above mentioned fix is required).

I've just used the latest version of branch deadlock-analysis (commit: 808d234d, which is from July 2016) and built the SW as per instructions in COMPILING. goto-cc aborts with errors if I include a C++ header (e.g. iostream).

$ goto-cc -pthread main.cc -o thread_lock.64

file /usr/include/x86_64-linux-gnu/c++/7/bits/c++config.h line 235: parse error before `; } namespace std'
file /usr/include/c++/7/bits/exception.h line 63: parse error before `) noexcept { }'
file /usr/include/c++/7/bits/exception.h line 64: parse error before `; virtual const char'
file /usr/include/c++/7/bits/exception.h line 74: parse error before `} extern  {'
file /usr/include/c++/7/exception line 57: parse error before `; } ; typedef'
file /usr/include/c++/7/exception line 58: parse error before `} ; typedef void'
file /usr/include/c++/7/exception line 67: parse error before `; terminate_handler get_terminate ('
file /usr/include/c++/7/exception line 71: parse error before `noexcept ; void terminate'
file /usr/include/c++/7/exception line 76: parse error before `noexcept ; unexpected_handler set_unexpected'
file /usr/include/c++/7/exception line 79: parse error before `noexcept ; unexpected_handler get_unexpected'

Using

$ goto-cc -pthread -std=c++11 main.cc -o thread_lock.64

doesn't change that.

Without <iostream> the SW compiles and I can use

$ goto-instrument thread_lock.64 --show-deadlocks

My system is Linux 64 bit with gcc 7.3.

[tautschnig]

This was fixed in #2364 (and further extended in #6402). The issues noticed by @sschwarzmann, however, remain (and are documented in various issues filed against this project): our C++ front-end requires work to fully support C++11 and later.