| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-04-04 | Remove linechart for klee-stats | Timotej Kapus | |
| 2019-04-04 | Add add -grafana option to klee-stats | Timotej Kapus | |
| It starts a simple web server that acts as a simple JSON datasource for grafana | |||
| 2019-04-04 | Change the .stats format into sqlite3 | Timotej Kapus | |
| Improves querying of the .stats file, reduces its size, speeds up reads and writes and has better defined fail behaviour. | |||
| 2019-04-02 | Add FreeBSD OS triple in RaiseAsm | Gleb Popov | |
| 2019-04-02 | Teach ConcreteTest.py to use `gmake` instead of `make` on FreeBSD | Gleb Popov | |
| 2019-04-02 | Handle __assert() function as handleAssertFail. This assert variant is used ↵ | Gleb Popov | |
| on FreeBSD | |||
| 2019-04-02 | Fix klee-replay tool on FreeBSD. | Gleb Popov | |
| 2019-04-02 | POSIX runtime fixes for FreeBSD. | Gleb Popov | |
| 2019-04-02 | Do not take sys/capability.h header into account on FreeBSD. Also use ↵ | Gleb Popov | |
| libutil.h header there. | |||
| 2019-04-02 | Fix build of Executor.cpp on FreeBSD. | Gleb Popov | |
| 2019-03-31 | Made test/Runtime/POSIX/GenBout.c run in an isolated directory | Andrew Santosa | |
| 2019-03-31 | Applied clang-format on tools/gen-random-bout/gen-random-bout.cpp | Andrew Santosa | |
| 2019-03-31 | Various updates to gen-random-bout.cpp | Andrew Santosa | |
| * Added handling of --sym-arg * Resolved the crash when minimum and maximum number of arguments for --sym-args are equal * Replaced "range" with "n_args" produced by --sym-args * Added model_version variable (constrained to 1), to prevent klee complaining about insufficient input * Allow a single dash to prefix an option * Arrange the elements in the correct order: command-line arguments, files, stdin, stdout * Added test/Runtime/POSIX/GenRandomBout.c test, with a substitution for %gen-random-bout in test/lit.cfg | |||
| 2019-03-21 | remove tests for LLVM <= 3.7 | Julian Büning | |
| 2019-03-21 | drop support for LLVM <= 3.7 | Julian Büning | |
| 2019-03-21 | remove copy of ScalarizerPass for LLVM 3.4 | Julian Büning | |
| 2019-03-21 | remove obsolete LegacyLLVMPassManagerTy | Julian Büning | |
| 2019-03-21 | remove obsolete macro KLEE_LLVM_GEP_TYPE | Julian Büning | |
| 2019-03-20 | tests: add STPDumpDebugQueries.c | Frank Busse | |
| 2019-03-20 | STPSolver: C++11, add missing free, refactoring | Frank Busse | |
| 2019-03-20 | Moving to version 2.1-pre | Cristian Cadar | |
| 2019-03-19 | Release notes for 2.0 v2.0 | Cristian Cadar | |
| 2019-03-19 | Set version to 2.0! | Cristian Cadar | |
| 2019-03-19 | Add support to assign debug instructions to optimised code | Martin Nowack | |
| 2019-03-19 | Use debugging information from newer LLVM versions | Martin Nowack | |
| 2019-03-19 | separate between instructions and functions | Martin Nowack | |
| 2019-03-19 | Refactor InstructionInfoTable | Martin Nowack | |
| Better debug information | |||
| 2019-03-19 | Dockerfile: Add libcxx as a build dependency | MartinNowack | |
| 2019-03-19 | Add Read consistency test case, spelling | Timotej Kapus | |
| 2019-03-19 | Fix representation of ReadExpr of equivalent arrays | Martin 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-18 | Update Dockerfile with new dependencies | Martin Nowack | |
| 2019-03-18 | Update dependencies | Martin Nowack | |
| 2019-03-18 | Disable optimisation for functions that contain KLEE calls | Martin 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-18 | make test/Feature/srem.c more explicit | Julian Büning | |
| 2019-03-17 | Fix `true` invocation in case docker image could not be pushed | Martin Nowack | |
| 2019-03-17 | Use newer uclibc version: libc++ requires locale support activated | Martin Nowack | |
| 2019-03-17 | Add 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-17 | Add libc++ as build dependency to KLEE | Martin Nowack | |
| 2019-03-17 | Cmake enhance detection of C++ libraries and include files | Martin Nowack | |
| * Use directory instead of libc++ files * support `bca` and `ba` files * Add additional checks if directories exist | |||
| 2019-03-17 | Fix libc++ testcases | Martin 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-17 | Added libcxx flag | Lukas Wölfer | |
| 2019-03-17 | Add support for libc++ as part of the build.sh scripts | Martin Nowack | |
| 2019-03-17 | Generalise clang package detection for linux and mac osx | Martin Nowack | |
| 2019-03-17 | Renamed --use-cache to --use-branch-cache | Cristian Cadar | |
| 2019-03-17 | run VerifierPass after optimization and instrumentation | Julian Büning | |
| 2019-03-16 | Added support for disabling --batch-instructions and --batch-time by setting ↵ | Cristian Cadar | |
| them to 0 | |||
| 2019-03-15 | Hiding general (LLVM) options in klee --help ! | Cristian Cadar | |
| 2019-03-15 | Placed option categories in the klee namespace and options in the anonymous ↵ | Cristian Cadar | |
| namespace in Executor.cpp | |||
| 2019-03-15 | Placed --max-time in the termination category | Cristian Cadar | |
| 2019-03-15 | Placed --rewrite-constraints in the constraint solving category | Cristian Cadar | |
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |