about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2021-09-10llvm11: Handle llvm.roundeven instrinsicLukas Zaoral
See: https://reviews.llvm.org/D75670
2021-09-10llvm12: Implement llvm.{s,u}{max,min} intrinsicsLukas Zaoral
The vector variants are not implemented at the moment. See: https://reviews.llvm.org/D84125 Co-authored-by: Lukas Zaoral <lzaoral@redhat.com> Co-authored-by: Martin Nowack <m.nowack@imperial.ac.uk>
2021-09-10CI: Use the latest release of CMakeLukas Zaoral
2021-09-10llvm12: Add LLVM 12 to Travis CI and GitHub ActionsLukas Zaoral
2021-09-10llvm12: Add LLVM 12 to lit.cfgLukas Zaoral
2021-09-10llvm12: VectorType::getNumElements() has been deprecatedLukas Zaoral
... and has already been removed from the LLVM 13 source tree. See: https://reviews.llvm.org/D78127 https://reviews.llvm.org/D95570
2021-06-19Test failure for WSL 1Pavel Yatcheniy
2021-05-10allocate memory objects for functionsJulian Büning
Before, we reused the llvm::Function* value in the target program, even though it stems from KLEE's own address space. This leads to non-deterministic function pointers, even with --allocate-determ. This issue was identified in the MoKLEE paper. Now, we allocate a memory object per function, for its (potentially) deterministic address. Mapping this address back to llvm::Functions is done by the legalFunctions map. Also, pointer width now depends on the target, not the host.
2021-05-10extend function pointer testJulian Büning
Part of the test was already disabled in the initial checkin. However, we do support function pointers if they are restricted to one or more possible values.
2021-05-04cirrus: update FreeBSD python dependenciesFrank Busse
2021-05-04tests: adjust to new summary outputFrank Busse
2021-05-04differentiate between partial and completed paths in summary and fix paths ↵Frank Busse
stats when not dumping states
2021-05-04test: count paths with -dump-states-on-halt=falseFrank Busse
2021-04-30posix runtime: add malloc checksFrank Busse
2021-04-29Fix erroneous klee-stats legend for --print-allJordy Ruiz
Only absolute times were displayed, and were marked as %. Fixes CexCacheTime, ForkTime and ResolveTime columns.
2021-04-20Replaced the time-based delay after which the max-static-*-pct checks are ↵Cristian Cadar
performed with one expressed in terms of number of forks.
2021-04-20Refactored maxStaticPctChecks into a sequence of conditions.Cristian Cadar
2021-04-20Test for -max-static-fork-pctCristian Cadar
2021-04-20Added a warning when forking is skipped due to MaxStatic*Pct limits being ↵Cristian Cadar
reached
2021-04-20Added -max-static-pct-check-delay to replace the hardcoded delay after which ↵Cristian Cadar
the MaxStatic*Pct checks are performed.
2021-04-20Refactored MaxStatis*Pct conditions into a separate function.Cristian Cadar
2021-04-20test/Concrete: Use Python 3 in ConcreteTest.py explicitlyLukas Zaoral
Some Linux distributions, e.g. Fedora, do not install the unversioned Python binary by default and Python 2 has been dead for more than a year.
2021-04-18klee-replay: Fix -Wformat-truncation warningLukas Zaoral
Increase the size of the buffer to PATH_MAX in create_link as that is the maximal possible length of fname and check whether output truncation occurred. Fixes: tools/klee-replay/file-creator.c: In function 'create_file': tools/klee-replay/file-creator.c:55:31: warning: '%s' directive output may be truncated writing up to 4095 bytes into a region of size 64 [-Wformat-truncation=] 55 | snprintf(buf, sizeof(buf), "%s.lnk", fname); | ^~ ...... 344 | target = tmpname; | ~~~~~~~ In file included from /usr/include/stdio.h:866, from tools/klee-replay/file-creator.c:16: /usr/include/bits/stdio2.h:70:10: note: '__snprintf_chk' output between 5 and 4100 bytes into a destination of size 64 70 | return __builtin___snprintf_chk (__s, __n, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 71 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2021-04-18tests: Invoke tools through their corresponding macrosLukas Zaoral
2021-04-18tests: Do not add klee tools to PATH in litLukas Zaoral
It may happen that some older instance of klee is already present in PATH. All tests that call plain klee instead of %klee may use it and then unexpectedly fail. This commit will make all tests that rely on klee tools being explicitly in PATH fail in our CI. From now on, only LLVM tools, FileCheck and not will be in lit's PATH.
2021-04-08cmake: Fix CMP0026 policy deprecation warningLukas Zaoral
CMake 3.19+ started to issue warnings if this policy is set to OLD: CMake Deprecation Warning at test/CMakeLists.txt:143 (cmake_policy): The OLD behavior for policy CMP0026 will be removed from a future version of CMake. The cmake-policies(7) manual explains that the OLD behaviors of all policies are deprecated and that a policy should be set to OLD only under specific short-term circumstances. Projects should be ported to the NEW behavior and not rely on setting a policy to OLD.
2021-03-05Add cmake custom target `uninstall`jiseongg
`make uninstall` is enabled. Without this, uninstalling was done manually with `rm` command.
2021-03-04[Z3] Handle the case when interruption caught by Z3Pavel Yatcheniy
2021-03-04tests: add support for LLVM 11.1Frank Busse
2021-03-04cmake: Fix warning about implicit type conversionLukas Zaoral
Fixes: CMake Warning (dev) at CMakeLists.txt:478 (set): implicitly converting 'String' to 'STRING' type. This warning is for project developers. Use -Wno-dev to suppress it.
2021-02-26Improved PR template by making it more succinct.Cristian Cadar
2021-02-22runtime/POSIX: fix failures with glibc-2.33Jiri Slaby
commit 8ed005daf0ab of glibc-2.33 (Remove stat wrapper functions, move them to exported symbols) removed renames of `__fxstat`, `__xstat`, and `__lxstat` to `__fxstat64`, `__xstat64`, and `__lxstat64`, respectively. But we relied on the renames to build `fd_64.c` properly. With glibc 2.33, we now see link failures of the POSIX runtime: error: Linking globals named '__xstat': symbol multiply defined! Rename the functions using `__REDIRECT_NTH` in the code as `__USE_FILE_OFFSET64` case (which we define at the top of the file by `#define _FILE_OFFSET_BITS 64`) did exactly that. Fixes #1384.
2021-02-16Executor: remove obsolete special case for __cxa_{re,}throwJulian Büning
__cxa_throw and __cxa_rethrow were not handled by special function handlers in the final version of #966 (which introduced support for C++ exception handling)
2021-02-16add klee_messages for C++ exception handling supportJulian Büning
otherwise, it is hard to tell whether EH support is available or not
2021-02-16add ifdefs for C++ exception handlingJulian Büning
restoring old behavior without EH support
2021-02-16renaming 'libcxx' -> 'libc++'Julian Büning
2020-12-23posix runtime: getcwd: check malloc and set errnoFrank Busse
* failing malloc was not handled before, now returns null/ENOMEM * when path is non-null and size is zero return null/EINVAL
2020-12-23tests: add getcwd EINVAL testFrank Busse
2020-12-23klee.h: fix compiler warnings (function declaration is not a prototype)Frank Busse
2020-12-23klee-libc: simplify mempcpyFrank Busse
2020-12-23posix runtime: remove dead branchFrank Busse
2020-12-18retire some build system legacyJulian Büning
2020-12-18fix cflags for runtime build typesJulian Büning
- `-DNDebug` -> `-DNDEBUG` - different flags for `Release{+Debug,}+Asserts` - `-g` is no longer part of common flags - `-D_DEBUG` is now only set for debug builds - removed unused `LIB_BC_FLAGS_{32,64}` - added example, architecture prefix for specific flags
2020-12-13FreeBSD CI: Use FreeBSD 12.2 instead of 12.1 and LLVM 9 instead of LLVM 8.Gleb Popov
2020-12-07Advancing version to 2.3-preCristian Cadar
2020-12-07Update version to 2.2 v2.2 2.2.xCristian Cadar
2020-12-07Release notes for v2.2Cristian Cadar
2020-12-04Only build 32bit runtime libraries if supported by platformMartin Nowack
Automatically detect if 32bit bitcode files can be built. In this case, build runtime library with 32bit as well.
2020-12-04llvm11: Add LLVM 11 to GitHub Actions and Travis CILukas Zaoral
2020-12-04llvm11: CallBase::getParamAlignment has been deprecatedLukas Zaoral
and should be replaced with CallBase::getParamAlign