Skip to content

Latest commit

 

History

History
88 lines (49 loc) · 3.71 KB

TROUBLESHOOTING.md

File metadata and controls

88 lines (49 loc) · 3.71 KB
Raw

Troubleshooting

This document covers some common issues with IKOS, and how to solve them.

Contact

[email protected]

Installation issues

"Could NOT find LLVM" while running cmake

CMake could not find LLVM.

First, install LLVM. This can usually be done with your package manager.

If this message still shows up, it means cmake cannot find the llvm-config command.

You can either add the LLVM binary directory in your PATH, or give cmake the full path to llvm-config, using -DLLVM_CONFIG_EXECUTABLE=/path/to/llvm-config

For instance, if you installed LLVM using Homebrew on Mac OS X, you can add LLVM in your path using:

$ PATH="$(brew --prefix)/opt/llvm/bin:$PATH"

"Could NOT find Clang" while running cmake

CMake could not find Clang.

First, install Clang. This can usually be done with your package manager.

If this message still shows up, it means cmake cannot find the clang command.

You can either add the clang binary directory in your PATH, or give cmake the full path to clang, using -DCLANG_EXECUTABLE=/path/to/clang

"Could not find ikos python module" while running ikos

The ikos command could not import the ikos python module.

The module should be under /path/to/ikos-install/lib/python*/site-packages

If the ikos python module is in another directory, make sure it is in your PYTHONPATH:

export PYTHONPATH=/path/to/ikos-python-module

"Two passes with the same argument (-domtree) attempted to be registered!" while running ikos

You are probably trying to build IKOS with shared libraries (using -DBUILD_SHARED_LIBS=ON) and LLVM was linked statically (using libLLVMxxx.a).

Unfortunately, this doesn't work because LLVM uses global constructors to register command line options, and the global constructors end up being called twice.

Compiling IKOS with both -DBUILD_SHARED_LIBS=ON and -DIKOS_LINK_LLVM_DYLIB=ON should fix the issue by linking against the libLLVM shared library.

"/usr/bin/ld: cannot find -lLLVMCore" while running Make

Your LLVM library was built as one single shared library libLLVM.so (LLVM_BUILD_LLVM_DYLIB=1), but CMake was configured to query specific library components and match link flags against them.

Compiling IKOS with both -DBUILD_SHARED_LIBS=ON and -DIKOS_LINK_LLVM_DYLIB=ON should fix the issue by linking against the single libLLVM shared library.

Analysis issues

Exited with signal SIGKILL

IKOS probably ran out of memory.

See Running ouf of memory

Running out of memory

IKOS might run out of memory on huge code bases.

Consider using the option --no-fixpoint-cache. It disables the cache of fixpoint for called functions, which decreases the memory usage at the cost of run time.

Known issues

Source Code Fortification

Source code fortification aims at making your source code more robust. It replaces regular memset(), memcpy() and memmove() calls to __memset_chk(), __memcpy_chk() and __memmove_chk(). According to Linux Standard Base Core Specification 4.1, the interfaces __memset_chk(), __memcpy_chk() and __memmove_chk() shall function in the same way as the interface memset(), memcpy() and memmove(), respectively, except that __memset_chk(), __memcpy_chk() and __memmove_chk() shall check for buffer overflow before computing a result. If an overflow is anticipated, the function shall abort and the program calling it shall exit.

The Buffer Overflow Analysis (BOA) in IKOS handles __memset_chk(), __memcpy_chk() and __memmove_chk() as unknown library functions, and won't report any warning. Consider using -D_FORTIFY_SOURCE=0 when you compile your source code to LLVM bitcode manually.