Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Multiple tests fail with "Option 'no-type-check' registered more than once!" #295

Open
TheBjoel2 opened this issue Nov 8, 2024 · 0 comments

Comments

@TheBjoel2
Copy link

I was trying to build ikos (master branch) on Arch Linux.
I did:

cmake \
-DCMAKE_BUILD_TYPE="Release" \
-DCMAKE_INSTALL_PREFIX="/usr" \
-DLLVM_CONFIG_EXECUTABLE="/usr/bin/llvm-config-14" \
-DAPPEND_GIT_VERSION=ON \
..

make

Which failed with a linker error:

[ 32%] Linking CXX executable ikos-pp
/usr/bin/ld: cannot find -lLLVMAggressiveInstCombine: No such file or directory
/usr/bin/ld: cannot find -lLLVMAnalysis: No such file or directory
/usr/bin/ld: cannot find -lLLVMAsmParser: No such file or directory
/usr/bin/ld: cannot find -lLLVMBitReader: No such file or directory
/usr/bin/ld: cannot find -lLLVMBitWriter: No such file or directory
/usr/bin/ld: cannot find -lLLVMCodeGen: No such file or directory
/usr/bin/ld: cannot find -lLLVMCore: No such file or directory
/usr/bin/ld: cannot find -lLLVMCoroutines: No such file or directory
/usr/bin/ld: cannot find -lLLVMInstCombine: No such file or directory
/usr/bin/ld: cannot find -lLLVMInstrumentation: No such file or directory
/usr/bin/ld: cannot find -lLLVMipo: No such file or directory
/usr/bin/ld: cannot find -lLLVMIRReader: No such file or directory
/usr/bin/ld: cannot find -lLLVMMC: No such file or directory
/usr/bin/ld: cannot find -lLLVMObjCARCOpts: No such file or directory
/usr/bin/ld: cannot find -lLLVMScalarOpts: No such file or directory
/usr/bin/ld: cannot find -lLLVMTarget: No such file or directory
/usr/bin/ld: cannot find -lLLVMTransformUtils: No such file or directory
/usr/bin/ld: cannot find -lLLVMVectorize: No such file or directory
collect2: error: ld returned 1 exit status

Reading through this, I assumed that the issue was the llvm built as one single shared library. Looking at how llvm is packaged on arch linux, that seemed to be true.
By adding -DBUILD_SHARED_LIBS=ON and -DIKOS_LINK_LLVM_DYLIB=ON to ikos cmake parameters,
and also including #include <array> into these files (There were several compiler errors):

core/test/unit/adt/patricia_tree/map.cpp
core/test/unit/domain/discrete_domain.cpp
core/test/unit/domain/numeric/congruence.cpp
core/test/unit/domain/numeric/constant.cpp
core/test/unit/domain/numeric/interval.cpp
core/test/unit/domain/numeric/interval_congruence.cpp

I was able to build it successfully.
However, after running make check, multiple tests failed

69% tests passed, 18 tests failed out of 59

Total Test time (real) =   2.12 sec

The following tests FAILED:
         42 - import-no-optimization (Failed)
         43 - import-basic-optimization (Failed)
         44 - import-aggressive-optimization (Failed)
         45 - analysis-buffer-overflow (Failed)
         46 - analysis-division-by-zero (Failed)
         47 - analysis-memory (Failed)
         48 - analysis-null-pointer-dereference (Failed)
         49 - analysis-assert-prover (Failed)
         50 - analysis-uninitialized-variable (Failed)
         51 - analysis-unaligned-pointer (Failed)
         52 - analysis-signed-int-overflow (Failed)
         53 - analysis-unsigned-int-overflow (Failed)
         54 - analysis-shift-count (Failed)
         55 - analysis-pointer-overflow (Failed)
         56 - analysis-pointer-compare (Failed)
         57 - analysis-function-call (Failed)
         58 - analysis-double-free (Failed)
         59 - analysis-soundness (Failed)
Errors while running CTest

Looking at logs to see why they're not passing, they seem to fail with the same error:

: CommandLine Error: Option 'no-type-check' registered more than once!

Maybe that is related to #61?

Also, it would be great if you tell us on which linux distro you build ikos so that we wouldn't have to deal with non-standard llvm distributions.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant