about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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
2019-03-13Documented options in ExprPPrinter.cpp and placed them into a new option ↵Cristian Cadar
category for building and printing expressions
2019-03-13Consistently use "default=true" and "default=false" instead of "default=on" ↵Cristian Cadar
and "default=off" in --help
2019-03-13Added options in QueryLoggingSolver.cpp to the constraint solving categoryCristian Cadar
2019-03-13Added missing description for some options in CmdLineOptions.cpp (and some ↵Cristian Cadar
reformatting).
2019-03-13Added options in CexCachingSolver.cpp to the constraint solving category and ↵Cristian Cadar
improved help messages
2019-03-13Created new search option category and moved there the options in ↵Cristian Cadar
UserSearcher.cpp
2019-03-13Added options in ArrayExprOptimizer.cpp to the constraint solving categoryCristian Cadar
2019-03-13Reordered includes in ArrayExprOptimizer.cpp for consistency with the other ↵Cristian Cadar
files
2019-03-13Created a new memory management option category for the options in ↵Cristian Cadar
MemoryManager.cpp
2019-03-13Renamed --warn-all-externals to --warn-all-external-symbols and placed it in ↵Cristian Cadar
the startup category
2019-03-13Renamed --no-output to --write-no-tests and placed it in the test case ↵Cristian Cadar
category (with --write-cov, --write-cvcs etc.)
2019-03-13Added --debug-log-state-merge to path merging categoryCristian Cadar
2019-03-12Add integer sanitizer to UBSanMartin Nowack
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-02-17 16:55:12 +0000