about summary refs log tree commit diff homepage
path: root/test
AgeCommit message (Collapse)Author
2021-09-10llvm12: Implement llvm.abs intrinsicLukas 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-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-10llvm12: Add LLVM 12 to lit.cfgLukas Zaoral
2021-06-19Test failure for WSL 1Pavel Yatcheniy
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-04tests: adjust to new summary outputFrank Busse
2021-05-04test: count paths with -dump-states-on-halt=falseFrank Busse
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-20Test for -max-static-fork-pctCristian 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-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-04tests: add support for LLVM 11.1Frank Busse
2021-02-16renaming 'libcxx' -> 'libc++'Julian Büning
2020-12-23tests: add getcwd EINVAL testFrank Busse
2020-12-23klee-libc: simplify mempcpyFrank Busse
2020-12-04Test reflecting the LLVM 11 behavior for transforming reads of the form ↵Cristian Cadar
f[k], with k symbolic and f a 4-element vector into something along the lines: if k == 0 => f[0] elif k == 1 => f[1] elif k == 2 => f[2] elif k == 3 => f[3] else ==> undef
2020-12-04Test reflecting the LLVM 11 behavior for transforming writes of the form ↵Cristian Cadar
f[k] = v, with f a 4-element vector, into something along the lines: if k == 0 => f[0] = v if k == 1 => f[1] = v if k == 2 => f[2] = v if k == 3 => f[3] = v
2020-12-04Move all overflows from the vector instructions tests into a new file, as ↵Cristian Cadar
the overflow behaviour is different in LLVM 11.
2020-12-04Add LLVM 11 to lit.cfgCristian Cadar
2020-12-02Detect system include headers on macOSMartin Nowack
System header files on macOS are not part of `/usr/include` since Catalina. Instead, multiple locations are possible and depend on the selected SDK. Use `xcrun` to automatically detect the correct path on macOS.
2020-11-11tests: add test for klee-stats --table-format=csv/readable-csvFrank Busse
2020-11-09Test checking that __strcpy_chk is handled correctly when uclibc is usedCristian Cadar
2020-11-09Test checking that __strcat_chk is handled correctly with klee-libcCristian Cadar
2020-11-09Added test checking that a simple overflow is caught via -D_FORTIFY_SOURCECristian Cadar
2020-11-09Test checking that __memchk_chk is handled correctly with the freestanding ↵Cristian Cadar
library.
2020-11-04[cmake] Remove several leftovers from old autoconf build systemMartin Nowack
2020-11-03fix: bcmp with n==0Alastair Reid
This was executing the loop when n==0 leading to an out of bound pointer error. Found while verifying Rust code that compares strings.
2020-10-30Add test for atexit orderTomas Jasek
2020-10-30Mark the StaticDestructor test as failing on macOSCristian Cadar
2020-10-30Optimize StaticDestructor test to be less fragile to compiler optimizations.Cristian Cadar
2020-10-12MergingSearcher: remove random-path incompatibilityFrank Busse
2020-10-12address MartinNowack's remaining feedbackJulian Büning
2020-10-12Exception handling only for LLVM >= 8.0.0Julian Büning
2020-10-12Implemented support for C++ ExceptionsFelix Rath
We implement the Itanium ABI unwinding base-API, and leave the C++-specific parts to libcxxabi. Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de>
2020-10-09implement fneg instructionJulian Büning
2020-10-09fix: fabs() working on the wrong argumentDavid Laprell
2020-10-09Add testcase for weakly linked globalsMartin Nowack
2020-10-06Added support for klee_open_merge and klee_close_merge in replay, together ↵Cristian Cadar
with a test case.
2020-09-30tests: add tests for empty .stats and additional/missing columnsFrank Busse
2020-09-30tests: support .test and introduce %klee-statsFrank Busse
2020-09-17Add test for klee-zestiTimotej Kapus
2020-09-02More robust handling of unknown intrinsicsAlastair Reid
- If an unknown intrinsic appears in the bitcode file, it is reported but execution can proceed. - If an unknown intrinsic is encountered during execution of some path, - the intrinsic is reported - this path is treated as an error - execution of other paths can proceed To be more precise, there is a list of "known unknown intrinsics". Intrinsics not on this list will prevent execution.
2020-08-28Definition of __cxa_thread_atexit_impl for the KLEE libc.Alastair Reid
This is a thread-local version of __cxa_atexit (but, in the absence of threads, it is sufficient to just call __cxa_atexit). The test is based on the existing test for atexit in test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c The motivation for adding this function is to support the Rust standard library that calls __cxa_thread_atexit_impl. This function is usually a weak symbol but, in KLEE, this behaves like a call to an unknown function and chaos ensues. Worse, it happens just as the program is cleanly shutting itself down, so programs that are cleanly exiting crash with the wrong message.
2020-08-07New intrinsic: klee_is_replayAlastair Reid
This instrinsic detects whether the program is being executed symbolically or concretely (i.e., using the libkleeRuntest library). The intended usage (illustrated in the test program) is to allow the test program to display the input values by invoking any libraries it wants to. This is especially valuable if you are constructing complex, structured values and for languages like Rust (or C++) that have rich libraries and print libraries. For example, you might pick a symbolic value N with the assumption "0 <= N < 10" and then pick N symbolic values and write them to an array. The resulting ktest file is a bit hard to understand compared with the output of the standard print function in Rust/C++.
2020-06-29Implement fshr/fshl intrinsicsAlastair Reid
Changes: - IntrinsicCleaner accepts fshr/fshl as accepted intrinsics - Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract - Klee/main suppresses warnings about externals that are LLVM reserved (i.e., begin with "llvm.") - New test exercises 32 and 7 bit versions including oversize shift values Test values are based on LLVM's test for fshl/fshr - Changes that depend on existence of fshr/fshl are guarded by #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) or ; REQUIRES: geq-llvm-7.0
2020-06-25Enforce fork/branch limits in branch() and fix double terminationFrank Busse
* extend help messages for -max-memory and -max-memory-inhibit * introduces branchingPermitted() * enforces fork/branch limits in branch() (vector version) * changes main loop * calls updateStates() before checkMemoryUsage() * calls updateStates() again in case we early terminate states This should prevent double termination for now. Other solutions are imho more expensive as we would have to compare possibly large vectors of states (either states(arr) in checkMemoryUsage() or removedStates in terminateState()).
2020-06-25fix Executor: initializeGlobalAliasesJulian Büning
2020-06-25add simple unknown bitcast alias test from the original issueJulian Büning
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-24 15:44:05 +0000