about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2018-07-04Fix compiler warnings if assertions are disabledMartin Nowack
2018-07-04Support sanitizer suppression files with lit-based testingMartin Nowack
2018-07-04Extensive updates to the build script for dependencies and dockerMartin Nowack
Building/managing dependencies of KLEE are not easy. This script should change this. Features: * script install different versions in their specific directories This allows: - to have different versions in parallel installed: llvm, solvers - to have different optimization levels installed (Debug, no-debug, assertions, optimized) - to have different versions of instrumentation enabled (address, memory, leakage, undefined behavior) * the script is kept distribution agnostic: assuming basic packages are installed (a compiler), use `scripts/build/ubuntu-dependencies.sh` to install ubuntu specific ones * the script does not install any file into system directories (sudo is not required) files are only installed into a user specified BASE directory The same scripts are used for either local setup (`scripts/build/local_install.sh`) or create a docker image based of your current source folder (`scripts/build/build_docker.sh`) Change the defaults permanently by modifying (`scripts/build/common-defaults.sh`) or change them on the fly by providing them as environment variables on the command line. The same scripts are also used for TravisCI, so we test what we are using.
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-21 13:59:15 +0000