about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2019-04-08Add LD_LIBRARY_PATH to docker image 2.0.xGerben Oolbekkink
Fixes #1080. The proper LD_LIBRARY_PATH is required when binaries linked with kleeRuntest are run. The STP line is changed to extend the library path instead of replace it, I am not sure if it can be removed at this moment.
2019-03-26Install tabulate when building.Gerben Oolbekkink
Fixes #1069. This makes the tabulate package available in the Docker image.
2019-03-19Release notes for 2.0 v2.0Cristian Cadar
2019-03-19Set version to 2.0!Cristian Cadar
2019-03-19Add support to assign debug instructions to optimised codeMartin Nowack
2019-03-19Use debugging information from newer LLVM versionsMartin Nowack
2019-03-19separate between instructions and functionsMartin Nowack
2019-03-19Refactor InstructionInfoTableMartin Nowack
Better debug information
2019-03-19Dockerfile: Add libcxx as a build dependencyMartinNowack
2019-03-19Add Read consistency test case, spellingTimotej Kapus
2019-03-19Fix representation of ReadExpr of equivalent arraysMartin Nowack
ObjectStates can be shared between multiple states. A read expression of a symbolic object can be represented differently depending on previous read expression on the same object. If the read expression uses a symbolic index, all pending updates will become entries in the update list of the object state. If the same object state is read again, with a concrete index, the latest update list item will be referenced, even though it might contain more recent but non-essential updates. If, instead, a concrete read will be executed first, it does not contain the non-essential updates. For both executions, the ReadExpr with a constant index will have two different representations, which is not intented. This patch makes sure, we do not include more recent, non-essential updates for concrete reads. Fixes #921
2019-03-18Update Dockerfile with new dependenciesMartin Nowack
2019-03-18Update dependenciesMartin Nowack
2019-03-18Disable optimisation for functions that contain KLEE callsMartin Nowack
Compilers are allowed to hoist function calls and do GVE. This is currently done even without `--optimization` enabled. This is unfortunate in the context of KLEE function calls that might depend on specific code position without direct control flow dependencies. In such cases, function calls can be hoisted. To circumvent this, disallow to optimise functions that contain such calls by default. This might reduce optimisation for some functions containing such function calls but still allows it for all others. This patch adds an additional pass, that detects all functions starting with a prefix `klee_` and disable optimisations for functions containing such calls. This is enabled by default but can be disabled by `--klee-call-optimisation=false`.
2019-03-18make test/Feature/srem.c more explicitJulian Büning
2019-03-17Fix `true` invocation in case docker image could not be pushedMartin Nowack
2019-03-17Use newer uclibc version: libc++ requires locale support activatedMartin Nowack
2019-03-17Add travis support to build with libc++Martin Nowack
Enable libc++ support by default but disable for LLVM < 3.7 as not supported. Disable support for Mac OSX: wllvm is not working well with dylib but Mac OSX currently requires dynamic version compiled. In general it should be possible, maybe later version.
2019-03-17Add libc++ as build dependency to KLEEMartin Nowack
2019-03-17Cmake enhance detection of C++ libraries and include filesMartin Nowack
* Use directory instead of libc++ files * support `bca` and `ba` files * Add additional checks if directories exist
2019-03-17Fix libc++ testcasesMartin Nowack
* remove wrapper script invocation and script * add build instruction to test cases * added additional checks * add check to avoid execution of tests if KLEE is not compiled with libc++
2019-03-17Added libcxx flagLukas Wölfer
2019-03-17Add support for libc++ as part of the build.sh scriptsMartin Nowack
2019-03-17Generalise clang package detection for linux and mac osxMartin Nowack
2019-03-17Renamed --use-cache to --use-branch-cacheCristian Cadar
2019-03-17run VerifierPass after optimization and instrumentationJulian Büning
2019-03-16Added support for disabling --batch-instructions and --batch-time by setting ↵Cristian Cadar
them to 0
2019-03-15Hiding general (LLVM) options in klee --help !Cristian Cadar
2019-03-15Placed option categories in the klee namespace and options in the anonymous ↵Cristian Cadar
namespace in Executor.cpp
2019-03-15Placed --max-time in the termination categoryCristian Cadar
2019-03-15Placed --rewrite-constraints in the constraint solving categoryCristian Cadar
2019-03-15Categorized the options in SpecialFunctionHandler.cppCristian Cadar
2019-03-15Added help message for --use-constant-arrays, and placed option in the ↵Cristian Cadar
constraint solving category
2019-03-15Placed --exit-on-error, --max-tests and --watchdog in the termination categoryCristian Cadar
2019-03-15Renamed --seed-out to --seed-file and --seed-out-dir to --seed-dir, and ↵Cristian Cadar
placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace.
2019-03-15Reformatted options and headers in Executor.cpp and did a proofreading pass ↵Cristian Cadar
over all help messages.
2019-03-15Added several options in Executor.cpp to the constraint solving categoryCristian Cadar
2019-03-15Created a new statistics option categoryCristian Cadar
2019-03-15Moved the options in Optimize.cpp to the module categoryCristian Cadar
2019-03-15Created a new module-related option category and moved the options in ↵Cristian Cadar
KModule.cpp in there
2019-03-13Hide the general category (with LLVM options) in Kleaver.Cristian Cadar
2019-03-13Added function to hide all options in a given category. Removed uneeded ↵Cristian Cadar
(and incorrectly-implemented) function for hiding all options unrelated to a set of categories.
2019-03-13Placed --warnings-only-to-file in a miscellaneous categoryCristian Cadar
2019-03-13Placed --use-visitor-hash in the expresion building/printing categoryCristian Cadar
2019-03-13Renamed directoryToWriteQueryLogs to DirectoryToWriteQueryLogs (and some ↵Cristian Cadar
reformatting)
2019-03-13Renamed --red-zone-space to --redzone-size and improved help messageCristian Cadar
2019-03-13Added --const-array-opt to building&printing expression categoryCristian Cadar
2019-03-13Renamed --use-construct-hash to --use-construct-hash-stp and moved it and ↵Cristian Cadar
use-construct-hash-z3 to the expression building/printing category
2019-03-13Moved options in kleaver/main.cpp in either the constraint solving or the ↵Cristian Cadar
expression building/printing category
2019-03-13Moved options in ExprSMTLIBPrinter.cpp to the expression building and ↵Cristian Cadar
printing category
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-05-20 08:41:15 +0000