seahorn / sea-dsa

A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Other
157 stars 29 forks source link

Question about building sea-dsa #67

Closed shaobo-he closed 4 years ago

shaobo-he commented 4 years ago

Hello sea-dsa developers,

I encountered errors in building sea-dsa inside SMACK. I simply added add_subdirectory(sea-dsa) to SMACK's CMakeLists.txt file and cmake will complain something like Unknown CMake command "add_llvm_library".. I think this is because sea-dsa requires definitions from LLVM, which are provided using these commands (https://github.com/seahorn/sea-dsa/blob/master/CMakeLists.txt#L87-L92). However, these commands only take effects when sea-dsa is built at the top level. So I was wondering if these lines should be moved below the if block where they are currently in.

agurfinkel commented 4 years ago

The expectation is that any external project that wraps sea-dsa will provide the necessary definition for the LLVM version to use. Sea-Dsa can only detect which version of LLVM to use when it is build in stand alone mode.