about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2018-07-04runtime: remove obsolete code for building modules instead of archivesJulian Büning
2018-07-04Reorder linking and optimizationsMartin Nowack
Link intrinsic library before executing optimizations. This makes sure that any optimization run by KLEE on the module is executed for the intrinsic library as well. Support .ll files as input for KLEE as well.
2018-07-04Reorganise runtime libraries provided by KLEEMartin Nowack
Strictly differentiate between the following type of libraries: * FreeStanding: contains minimal amount of methods a compiler would expect * klee-libc: contains a minimal libc implementation * POSIX: contains a POSIX layer that can be used on top of a libc implementation * Intrinsic: contains additional runtime functions which provide KLEE-specific functionalities, (e.g. checks) Builds always archives instead of single modules. This allows to reduce linked-in dependencies of tested applications.
2018-07-02Removed obsolete scriptCristian Cadar
2018-07-02test/lit.cfg: remove obsolete hack from (LLVM < 3.0 is no longer supported)Julian Büning
2018-07-02CMake: use cmake_{push,pop}_check_stateJulian Büning
2018-07-02CMake: check for ctype and mallinfo functions with CXX instead of C compilerJulian Büning
2018-06-29fix out of range access in KleeHandler::getKTestFilesInDirFrank Busse
2018-06-29Explicitly initialize value to squelch a potentially uninitialized value warningDaniel Schemmel
2018-06-29Fix the final -Wimplicit-fallthrough warningDaniel Schemmel
2018-06-29Make ConstantExpr hashing function faster and modify affected testTimotej Kapus
2018-06-14Add unittest for DiscretePDFMartin Nowack
2018-06-13klee_int: allow NULL as nameFrank Busse
2018-06-11cmake: find_llvm, handle libLLVM-version.so properlyJiri Slaby
Some builds of llvm contain a lib like this: /usr/lib64/libLLVM-3.9.so Extend the regular expression, so that we really return what we are supposed to. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-06-11Fixed memory leak from Executor::inCloseMerge, fixes #883Lukas Wölfer
2018-05-24isLSB should be a boolean, as it is only used in truth contextsDaniel Schemmel
2018-05-24remove switch fallthrough in floating point comparisionDaniel Schemmel
2018-05-24llvm37: enable travis testingJiri Slaby
Suggested by @MartinNowack in #681. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-05-24llvm37: handle getRegisteredOptionsJiri Slaby
In LLVM 3.7 and later, getRegisteredOptions takes no arguments and returns the map directly. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-05-24test: add versions of some tests for LLVM 3.7Richard Trembecký
Clone some tests to have their 3.7 version. 'call's, 'load's and 'getelementptr's match the new specification in them. @andreamattavelli: Fixed test cases: BitCastAlias test cases included modification to alias specifications that require LLVM 3.8 [v2] added comments what was changed and why [v3] the new tests are without suffix, the old ones have ".leq36". Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-05-24llvm: make KLEE compile against LLVM 3.7Richard Trembecký
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-05-24llvm37: handle GetElementPtrInst::Create's new parameterJiri Slaby
LLVM 3.7 added a PointeeType parameter to GetElementPtrInst::Create. Let's handle that by a macro called KLEE_LLVM_GEP_TYPE, defined in Version.h. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-05-23test: add parenthesis around & operandsJiri Slaby
Some compilers are picky, so avoid the warning by additional parentheses: test/VectorInstructions/integer_ops_unsigned_symbolic.c:85:22: warning: & has lower precedence than <; < will be evaluated first [-Wparentheses] Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-05-22clang-format on lib/Module/{IntrinsicCleaner.cpp,Passes.h}Julian Büning
2018-05-22some housekeeping in Passes.h and IntrinsicCleaner.cppJulian Büning
This commit addresses the following: * remove unused variables block_split (::runOnBasicBlock) and LI (::IntrinsicCleanerPass) in IntrinsicCleanerPass * add `dirty = true` to `Intrinsic::vacopy` case * use `eraseFromParent()` methods instead of `removeFromParent()` and `delete` * add `override` keyword to `runOn{Module,Function}` methods
2018-05-22CompressionStream: fix sporadic segfaults (uninitialised avail_in)Frank Busse
2018-05-22Removed .c_str() from getSourceLocation callsCristian Cadar
2018-05-22Renamed printFileLine to getSourceLocation (as suggested by @delcypher) to ↵Cristian Cadar
reflect the fact that it simply returns a string
2018-05-22Simplified printFileLine by using std::to_string, and removed unneeded ↵Cristian Cadar
version that takes an argument a stream
2018-05-21stop using DEBUG macro nameJiri Slaby
This is too generic and llvm 6.0 defines DEBUG as follows: #define DEBUG(X) DEBUG_WITH_TYPE(DEBUG_TYPE, X) This then results in various build failures where once the macro is defined, once it is not. So rename this generic macro to KLEE_ARRAY_DEBUG. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-05-21fix some casts for LLP64 compilersFrank Busse
2018-05-18tests: use names in klee_make_symbolicFrank Busse
2018-05-18Delete coverageServer.pyTimotej Kapus
Delete the old coverage gathering code. Unneccessary with move to codecov.
2018-05-17Abort execution if --only-output-states-covering-new is enabled but its ↵Cristian Cadar
dependency --output-istats is not
2018-05-17Add support for concretizing symbolic objects passed to external functionsTimotej Kapus
2018-05-17Improve error messages for ReadStringAtAddressTimotej Kapus
2018-05-15Improved code qualityLukas Wölfer
2018-05-15Implemented incomplete mergingLukas Wölfer
2018-05-15remove QueryLog.hFrank Busse
2018-05-12Update clang-format standard for KLEE codebase to C++11Martin Nowack
2018-05-09Fix test case to check for correct call stringMartin Nowack
2018-05-09Improve handling of constant array in Z3Timotej Kapus
2018-05-09Remove the option for truncating lines in assembly.llMartin Nowack
The behaviour couldn't be triggered for a kcachegrind from 2012.
2018-05-09Remove workaround for bug in older LLVM version (< 3)Martin Nowack
2018-05-09Fix include filesMartin Nowack
2018-05-08remove unused file: tools/klee/Debug.cppDaniel Schemmel
2018-05-07Fixed test case to exercise modification to utimes()Cristian Cadar
2018-05-07Fixed utimes() behavior for symbolic files when the second argument is NULLyxliang01
2018-05-06Moved regression test to proper location. Fixes #705Cristian Cadar
2018-05-05Fix handling of errno if external functions are invokedMartin Nowack
If an external function in KLEE is invoked, it might update errno. Previously, the errno specific variable in a state was only updated if it was part of the executed instructions. That opened up a timeframe that increased the likelihood of errno being overwritten by another method call. This patch fixes two issues: * the errno of the KLEE process state is updated before the external function call allowing to detect changes to it later on * after the external call, the memory object of errno is directly updated with its new value, reducing the likelihood to be overwritten by another call Additional features: * Add support for `errno()` for Darwin as well. * Simplified errno handling in POSIX layer