search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
811 stars 257 forks source link

centos compile cbmc 6.0.1 failed #8373

Closed niuzhi closed 1 month ago

niuzhi commented 1 month ago

CBMC version:6.0.1 Operating system:Centos Exact command line resulting in the issue: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ && cd build; ninja -j2 What behaviour did you expect: compile failed What happened instead:

Hello,CBMC developers,I am using the following command to compile and build cbmc on the CentOS operating system, but it always fails after several attempts. Could you help me solve this problem?Looking forward to your reply

command：cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ && cd build; ninja -j2

compile report this error information： image

Gcc/g++ version：8.5.0 flex 2.6.1 bison 3.0.4 cmake version 3.11.4

kroening commented 1 month ago

I did set up a build for ebmc for CentOS here: https://github.com/diffblue/hw-cbmc/blob/f2f3a40951f9e505a90621b430035b811dfc2b1a/.github/workflows/pull-request-checks.yaml#L110 Try make CXX="g++ -Wno-class-memaccess" LIBS="-lstdc++fs" -C src

niuzhi commented 1 month ago

@kroening The error still exists。 command： cmake -S . -Bbuild -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -DWITH_JBMC=OFF

make CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs" -C src -j4

image

tautschnig commented 1 month ago

With cmake you'll want:

cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -DCMAKE_EXE_LINKER_FLAGS=-lstdc++fs
cd build; ninja -j2
tautschnig commented 1 month ago

Resolving as guidance has been provided and no further questions have been raised since.

niuzhi commented 1 month ago

@tautschnig this question still exists

command：cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -DCMAKE_EXE_LINKER_FLAGS=-lstdc++fs -DWITH_JBMC=OFF

gcc version： gcc (GCC) 8.5.0 20210514 (Red Hat 8.5.0-22) Copyright (C) 2018 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. image

Can you provide a centos dockerfile?thanks

tautschnig commented 1 month ago

My apologies, it seems you need to use -DCMAKE_CXX_STANDARD_LIBRARIES instead of -DCMAKE_EXE_LINKER_FLAGS as otherwise the library ends up in the wrong place in the order of command-line arguments. So it should be

cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs -DWITH_JBMC=OFF

Please re-open if this still doesn't work.