seahorn/crab

Does crab support running on MacOS?

chenxi-yang opened this issue · 8 comments

chenxi-yang commented

If so, is there any related installation document on MacOS? Thank you very much!

caballa commented

The installation is done by CMake and it works for both MacOS and some Linux distributions such as Ubuntu. These are the steps as described in README.md.

mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=_INSTALL_DIR_ ../
cmake --build . --target install

Let me know if you have any problem. I'm happy to help.

  • 👍1
chenxi-yang commented

Hi I was trying to install apron on Mac OS with steps in README.md

I got

Command failed: 2

'make' 'CC=/Library/Developer/CommandLineTools/usr/bin/cc' 'CXX=/Library/Developer/CommandLineTools/usr/bin/c++' 'IS_VECTOR=-DVECTOR' 'APRON_PREFIX=[workspace]/Documents/workspace/crab/build/run/apron' 'GMP_PREFIX=/usr/local' 'MPFR_PREFIX=/usr/local'

See also

[workspace]/Documents/workspace/crab/build/apron-prefix/src/apron-stamp/apron-build-*.log

make[3]: *** [apron-prefix/src/apron-stamp/apron-build] Error 1
make[2]: *** [CMakeFiles/apron.dir/all] Error 2
make[1]: *** [CMakeFiles/apron.dir/rule] Error 2

when I run
cmake --build . --target apron && cmake

I assume this is something wrong with the cmake, but
cmake --build . --target ldd && cmake ..
works well.

(Not sure whether this problem is related to crab. I thought it might be helpful to post it here.

chenxi-yang commented

I tried

xcode-select --install && sudo ln -s /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/* /usr/local/include/

both do not work.

caballa commented

Regarding apron, can you share /Documents/workspace/crab/build/apron-prefix/src/apron-stamp/apron-build-*.log ?

Regarding the last comment, this is for making sure that C header files can be found. This has nothing to do with Crab. It will be needed if you want to compile C/C++ code on your mac.

chenxi-yang commented

Sure.

The log in /Documents/workspace/crab/build/apron-prefix/src/apron-stamp/apron-build-err.log is,
Undefined symbols for architecture x86_64: "_ap_policy_manager_alloc", referenced from: _box_policy_manager_alloc in box_policyMPQ.o "_itv_meet_ap_tcons0_array_MPQ", referenced from: _box_meet_tcons_array in box_meetjoinMPQ.o ld: symbol(s) not found for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) make[5]: *** [libboxMPQ.so] Error 1 make[4]: *** [c] Error 2

chenxi-yang commented

A update.
After reinstalled brew and cmake.
The same error occurs. But the log varies. This time, the log in /Documents/workspace/crab/build/apron-prefix/src/apron-stamp/apron-build-err.log is,

'
1 In file included from itv.c:5:
2 ./itv.h:8:10: fatal error: 'stdio.h' file not found
3 #include <stdio.h>
4 ^~~~~~~~~
5 1 error generated.
6 make[5]: *** [itvMPQ.o] Error 1
7 make[4]: *** [c] Error 2
'

caballa commented

The C header files cannot be found. It's a OS problem.
Which Mac OS version are you using?

If you have mojave you can also try:

open /Library/Developer/CommandLineTools/Packages/macOS_SDK_headers_for_macOS_10.14.pkg
chenxi-yang commented

Hi,
Thanks for your help.

Yes, it is a linking problem in Mac OSX. I am using Catalina, OS X 10.15.
After searching around, one solution works well.