Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-11-04 | Remove the duplicated check for DebugInfoIntrinsic | Hui Peng | |
2019-10-31 | Executor: fix missing default case in switch instruction | Frank Busse | |
2019-10-31 | LLVM 9.0: fourth parameter for @llvm.objectsize() | Julian Büning | |
2019-10-31 | support compilation against LLVM 9.0 | Julian Büning | |
2019-10-29 | ExecutorTimers: refactor and move to support lib | Frank Busse | |
- moves timer handling from Executor into support lib - introduces TimerGroup, removes TimerInfo/WriteStatsTimer/UpdateReachableTimer/WriteIStatsTimer classes - removes ExecutorTimers.cpp and ExecutorTimerInfo.h - removes -max-instruction-time flag (see #1114) | |||
2019-10-29 | ExecutorTimers: remove signalling, fix endless looping fork | Frank Busse | |
- adds -timer-interval threshold for timer checks - fixes #831 | |||
2019-10-08 | Executor.h: remove defined functions without implementation | Frank Busse | |
2019-09-20 | refactor PTree: use unique_ptr | Frank Busse | |
2019-09-20 | refactor PTree: remove split(), add attach() method | Frank Busse | |
2019-09-20 | Add saturated arithmetic intrinsics | Mateusz Naściszewski | |
2019-09-03 | Moved solver-related header files into a separate klee/Solver/ directory. | Cristian Cadar | |
2019-09-03 | Moved ConstructSolverChain.cpp to the Solver library. | Cristian Cadar | |
2019-09-03 | Renamed CmdLineOptions.cpp to SolverCmdLine.cpp (in line with the associated ↵ | Cristian Cadar | |
header SolverCmdLine.h) and moved it to the Solver library. | |||
2019-08-15 | ExecutorTimers: move dumpStates/dumpPTree into Executor | Frank Busse | |
* creates two new methods: dumpStates, dumpPTree | |||
2019-08-14 | Update basic block iterator after deleting instruction; add test case | Martin Nowack | |
2019-08-14 | fixed bug in IntrinsicCleaner trap cleaner | Michael Bryman | |
2019-08-14 | Replace sprintf with snprintf throughout codebase | Cristian Cadar | |
2019-08-12 | StatsTracker: switch from TRUNCATE to WAL journal mode | Frank Busse | |
2019-08-01 | Renamed misspelled file | Cristian Cadar | |
2019-07-30 | Use #include "klee/..." (instead of #include <klee/...>) consistently. | Cristian Cadar | |
2019-07-30 | Consolidated Expr-related include files into a single include/klee/Expr ↵ | Cristian Cadar | |
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE. | |||
2019-07-23 | Refactor ConstraintManager to more modern coding standards | Daniel Schemmel | |
Eliminates -Wdeprecated-copy warnings Performed clang-format on touched file | |||
2019-07-23 | Refactor ValueRange to more modern coding standards | Daniel Schemmel | |
Eliminates -Wdeprecated-copy warnings Performed partia clang-format on touched file | |||
2019-06-04 | fix some incorrect first lines | Julian Büning | |
2019-06-04 | make endif guard naming consistent | Julian Büning | |
2019-06-04 | make include guard naming consistent | Julian Büning | |
2019-06-04 | Fixed identifiers used in ifdefs to (1) not use reserved names and (2) use a ↵ | Cristian Cadar | |
consistent naming convention | |||
2019-06-04 | Remove parenthesis around returns, as reported and discussed in #891 | Cristian Cadar | |
2019-05-31 | PTree: fix dump() method | Frank Busse | |
2019-05-30 | ExecutionState: remove fnAliases | Julian Büning | |
2019-05-30 | implement FunctionAliasPass | Julian Büning | |
2019-05-30 | remove klee_alias_function() | Julian Büning | |
this function can be used to modify the control flow of the program on different paths, enabling self-modifying code. | |||
2019-05-28 | Implement handling of the llvm.fabs intrinsic | Felix Rath | |
2019-04-04 | some minor refactorings | Frank Busse | |
2019-04-04 | Clean klee-stats, StatsTracker and cmake | Timotej Kapus | |
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 | Handle __assert() function as handleAssertFail. This assert variant is used ↵ | Gleb Popov | |
on FreeBSD | |||
2019-04-02 | Fix build of Executor.cpp on FreeBSD. | Gleb Popov | |
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 | STPSolver: C++11, add missing free, refactoring | Frank Busse | |
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 | 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 |