about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2018-10-23Added support for KLEE value-based array optimizationAndrea Mattavelli
2018-10-23Added support for KLEE index-based array optimizationAndrea Mattavelli
2018-10-17tests: disable CompressedExprLogging on zlib-less systemsFrank Busse
2018-10-16Small changes to commentsCristian Cadar
2018-10-16Added missing header to SolverCmdLine.h and clang-format itCristian Cadar
2018-10-16Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file is meant ↵Cristian Cadar
to have only solver options.
2018-10-10fix handling of failing external callsFrank Busse
Currently KLEE only handles the first segfault in external calls as it doesn't unblock SIGSEGV afterwards. This patch unblocks the signal and enables handling of multiple failing calls.
2018-10-10cmake/lit: add asan/non-asan, ubsan/non-ubsan flagsFrank Busse
2018-10-08cleanup headers, whitespaces, and typesFrank Busse
2018-10-08add support for klee-replay on OSXFrank Busse
* also adds klee-replay as dependency for systemtests
2018-10-07Workaround for flaky coverageMartin Nowack
Merge unittest coverage results and system tests coverage results into one coverage report.
2018-10-04kleeModule: always link irreader (required since llvm 3.3)Julian Büning
2018-10-04remove obsolete dependency of kleeModule on kleeCoreJulian Büning
2018-10-04config.h.cmin: remove obsolete cmakedefineJulian Büning
2018-10-03Marking resolve methods as constCristian Cadar
2018-10-03Refactored AddressSpace::resolve() by creating a new function ↵Cristian Cadar
AddressSpace::checkPointerInObject() that is called in both the forward and the backward searches. This makes the code more modular and removes a large part of duplicated code and should also address the non-deterministic coverage in the resolve() function which affects Codecov reports.
2018-09-30Fix a crash when the last running state is terminated during mergingLukas Wölfer
2018-09-29Changed code to create up to 100 properly-numbered symbolic arguments, and ↵Cristian Cadar
add a corresponding check.
2018-09-29Add checks for correct usage of the POSIX model, together with an associated ↵Cristian Cadar
test.
2018-09-27Revert lit to 0.6.0 version, as 0.7.0 misbehavesCristian Cadar
2018-09-20Removed unused fileCristian Cadar
2018-09-20Removed unused --sym-files 0 0 argument from FD_Fail test and rewrote the ↵Cristian Cadar
test to use FileCheck instead of grep
2018-09-20Updated IoCtl test to use --sym-stdin instead of --sym-files 0 x to make ↵Cristian Cadar
stdin symbolic and removed unused arguments to main.
2018-09-20Updated DirSeek test to use --sym-stdin instead of --sym-files 0 x to make ↵Cristian Cadar
stdin symbolic.
2018-09-20Silence an uninitialized variable compiler warning (and a tiny formatting ↵Cristian Cadar
change)
2018-09-18travis: enable LLVM 4 testingJiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-18llvm4: gep_type_iterator has no operator*Jiri Slaby
Starting with LLVM 4, we have getStructTypeOrNull(), so use it. operator* in post-4 will have a different semantics. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-18llvm4: PointerType is not SequentialTypeJiri Slaby
So handle the type specially whenever needed. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-18llvm4: use chrono helpers from LLVMJiri Slaby
LLVM 4 removes the old time interface and starts using the C++11's chrono. So switch to that in klee for LLVM 4 too. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-18llvm4: errorOr and similarJiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-18llvm4: APFloat members are functionsJiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-18llvm4: handle different header namesJiri Slaby
LLVM 4 renamed and splitted some headers. Take this into account in includes. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-14travis CI: add LLVM 3.9 build testsJiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-14llvm39: switch KLEE_RUNTIME_BUILD_TYPE to Debug+AssertsJiri Slaby
So that we do not optimize the library during build. It should be optimized only on runtime, depending on the -optimize parameter. It could cause various failures like: inlinable function call in a function with debug info must have a !dbg location call void @klee_overshift_check(i64 64, i64 %int_cast_to_i64) Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-14cmake: find_llvm, fix libraries with llvm-config 3.9Jiri Slaby
llvm-config from llvm 3.9 was broken. Fix handling of improperly returned libraries. From: liblibLLVM-3.9.so.so To: libLLVM-3.9.so Fixes #895. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-14llvm: make KLEE compile against LLVM 3.9Jiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-10Add testcase to run POSIX environment and main without argumentsMartin Nowack
2018-09-10Add POSIX runtime as dependency for the test caseMartin Nowack
2018-09-10Unify the error message if that function has not been found.Martin Nowack
2018-09-10Fix generation of global constructors and destructorsMartin Nowack
Validate if the user-selected entry function exists. Do not assume it is `main`.
2018-09-10POSIX: Add invocation of klee_init_env into wrapper before calling mainMartin Nowack
To enable the POSIX support, the former implementation instrumented the main function and inserted a call to `klee_init_env` at the beginning. This has multiple disadvantages: * debugging information was not correctly propagated leaving the call to `klee_init_env` without debug information * the main function always required `int arg, char**` as part of the function definition of `main` Based on the new linking infrastructure, we can now add an additional wrapper `__klee_posix_wraper(int, char**)` that gets always called when POSIX support is enabled. It executes `klee_init_env` and after that calls the `main` function. Enabling POSIX support only requires the renaming of the user provided `main` into `__klee_posix_wrapped_main` in addition to linking.
2018-09-06Fix missing includes and declarationsMartin Nowack
2018-09-06Use FileCheck and LINE instead of grep if possibleMartin Nowack
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers.
2018-09-06llvm36.patch: fix build for newer glibc/gcc versionsFrank Busse
2018-09-06runtime: fix memory error in canonicalize_file_nameFrank Busse
Fixes #46 and reverts #47. As stated in #46, the solution works for musl, glibc etc. However, the code in stub.c is executed by uclibc and uclibc doesn't allocate the target buffer in realpath. The memory error occured while running df for 10min with DFS.
2018-09-06Build on trusty without sudo - uses faster Docker infrastructure from TravisCIMartin Nowack
2018-09-06Avoid Vararg non-deterministic allocationMartin Nowack
Vararg test can fail if KLEE is able to resolve the intended out-of-bound memory address to a memory object. To avoid this, allocate memory explicitly deterministic with sufficient space between the allocations. Enables support for Mac OSX again
2018-08-29klee-stats: add TResolve(%) to --print-allFrank Busse
2018-08-12llvm.sh: fix patch source pathsFrank Busse
2018-08-03Disabled unit testing in default buildAndrea Mattavelli
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 22:56:41 +0000