Issues including algorithm with cpp 11 about esbmc

[rafaelsamenezes]

Maybe it's time to switch the default version for releases

I agree. Ubuntu 24.04 also has 14 up to 18 in their distribution.

[lucasccordeiro]

@rafaelsamenezes : You're using an old version of ESBMC. With the current version, you should get:

$ esbmc alex3.cpp --std c++11
ESBMC version 7.6.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing alex3.cpp
Converting
Generating GOTO Program
GOTO program creation time: 0.730s
GOTO program processing time: 0.002s
Starting Bounded Model Checking
Symex completed in: 0.003s (19 assignments)
Slicing time: 0.000s (removed 19 assignments)
Generated 0 VCC(s), 0 remaining after simplification (0 assignments)
BMC program time: 0.003s

VERIFICATION SUCCESSFUL

[fbrausse]

There is an #if switch in the <algorithm> / <utility> header that conditionally defers to <type_traits> in order to provide std::swap for C++ >= 11. We don't provide our own <type_traits> (anymore). Thus, it might be that the installed header doesn't contain a std::swap definition. I'd need to know the package/version installed in order to fix this. Inquiry has been sent.

[fbrausse]

Just got a confirmation that their GCC-12.1 is installed in a non-standard location. We might need to pass --gcc-install-dir and/or --gcc-toolchain through to Clang in order or it to select the right GCC installation.

I actually would argue for a general pass-through option like -Xclang $OPT or -Wc,$OPTS s.t. we can easily let users add options to the clang command line related to their environment.

[fbrausse]

Indeed, old version being selected, GCC-4.8 (note, this is ESBMC v7.6, see #1837):

ESBMC version 7.5.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing main.cpp
clang invocation: 'clang-tool' '-isystem' '/tmp/esbmc.dfc9-b43b-4cb2/headers' '-isystem' '/tmp/esbmc-headers-6384-40b7-b898' '-m64' '-Dpthread_join=pthread_join_noswitch' '-Dpthread_mutex_lock=pthread_mutex_lock_noassert' '-Dpthread_mutex_unlock=pthread_mutex_unlock_noassert' '-Dpthread_cond_wait=pthread_cond_wait_nocheck' '-Dsem_wait=sem_wait_nocheck' '-v' '-target' 'x86_64-unknown-linux' '--sysroot=' '-D__builtin_memcpy=memcpy' '-D__ESBMC_alloca=__builtin_alloca' '-D__NO_CTYPE' '-fbracket-depth=1024' '-Wno-unknown-attributes' '-fsyntax-only'
clang version 11.0.0 (https://github.com/llvm/llvm-project.git [github.com] 0160ad802e899c2922bc9b29564080c22eb0908c)
Target: x86_64-unknown-linux
Thread model: posix
InstalledDir:
Found candidate GCC installation: /usr/lib64/gcc/x86_64-suse-linux/4.8
Selected GCC installation: /usr/lib64/gcc/x86_64-suse-linux/4.8
Candidate multilib: .;@m64
Candidate multilib: 32;@m32
Selected multilib: .;@m64
clang Invocation:
"clang-tool" "-cc1" "-triple" "x86_64-unknown-linux" "-fsyntax-only" "-disable-free" "-disable-llvm-verifier" "-discard-value-names" "-main-file-name" "main.cpp" "-mrelocation-model" "static" "-mframe-pointer=all" "-fmath-errno" "-fno-rounding-math" "-mconstructor-aliases" "-munwind-tables" "-target-cpu" "x86-64" "-fno-split-dwarf-inlining" "-debugger-tuning=gdb" "-v" "-resource-dir" "lib/clang/11.0.0" "-isystem" "/tmp/esbmc.dfc9-b43b-4cb2/headers" "-isystem" "/tmp/esbmc-headers-6384-40b7-b898" "-D" "pthread_join=pthread_join_noswitch" "-D" "pthread_mutex_lock=pthread_mutex_lock_noassert" "-D" "pthread_mutex_unlock=pthread_mutex_unlock_noassert" "-D" "pthread_cond_wait=pthread_cond_wait_nocheck" "-D" "sem_wait=sem_wait_nocheck" "-D" "__builtin_memcpy=memcpy" "-D" "__ESBMC_alloca=__builtin_alloca" "-D" "__NO_CTYPE" "-I" "/tmp/esbmc-cpp-headers-f923-9cd9-98fc" "-I" "/tmp/esbmc-cpp-headers-f923-9cd9-98fc/CUDA" "-I" "/tmp/esbmc-cpp-headers-f923-9cd9-98fc/Qt" "-I" "/tmp/esbmc-cpp-headers-f923-9cd9-98fc/Qt/QtCore" "-internal-isystem" "/usr/lib64/gcc/x86_64-suse-linux/4.8/../../../../include/c++/4.8" "-internal-isystem" "/usr/lib64/gcc/x86_64-suse-linux/4.8/../../../../include/c++/4.8/x86_64-suse-linux" "-internal-isystem" "/usr/lib64/gcc/x86_64-suse-linux/4.8/../../../../include/c++/4.8/backward" "-internal-isystem" "/usr/local/include" "-internal-isystem" "lib/clang/11.0.0/include" "-internal-externc-isystem" "/include" "-internal-externc-isystem" "/usr/include" "-Wno-unknown-attributes" "-std=c++11" "-fdeprecated-macro" "-fdebug-compilation-dir" "/nfs/site/disks/sdg74_0103/sparsaro/latest/esbmc_work" "-fbracket-depth" "1024" "-ferror-limit" "19" "-fgnuc-version=4.2.1" "-fcxx-exceptions" "-fexceptions" "-faddrsig" "-x" "c++" "main.cpp"
 
ignoring nonexistent directory "lib/clang/11.0.0/include"
ignoring nonexistent directory "/include"
#include "..." search starts here:
#include <...> search starts here:
/tmp/esbmc-cpp-headers-f923-9cd9-98fc
/tmp/esbmc-cpp-headers-f923-9cd9-98fc/CUDA
/tmp/esbmc-cpp-headers-f923-9cd9-98fc/Qt
/tmp/esbmc-cpp-headers-f923-9cd9-98fc/Qt/QtCore
/tmp/esbmc.dfc9-b43b-4cb2/headers
/tmp/esbmc-headers-6384-40b7-b898
/usr/lib64/gcc/x86_64-suse-linux/4.8/../../../../include/c++/4.8
/usr/lib64/gcc/x86_64-suse-linux/4.8/../../../../include/c++/4.8/x86_64-suse-linux
/usr/lib64/gcc/x86_64-suse-linux/4.8/../../../../include/c++/4.8/backward
/usr/local/include
/usr/include
End of search list.
In file included from main.cpp:1:
/tmp/esbmc-cpp-headers-f923-9cd9-98fc/algorithm:1169:12: error: no member named 'swap' in namespace 'std'
      std::swap(*j, *(j - 1));
      ~~~~~^

[fbrausse]

--gcc-install-dir only supported by clang version 15 and higher, though. Maybe it's time to switch the default version for releases. Our CI has been green for a clang-16 build for a while now. Here is another reason to update the frontend to v15+: #1585 (comment)