Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-07-11 | Removed support for klee_make_symbolic with 2 arguments. This has been ↵ | Cristian Cadar | |
deprecated for many years now and causes problems during replay. Changed and simplified affected test case. | |||
2018-07-04 | Fix compiler warnings if assertions are disabled | Martin Nowack | |
2018-07-04 | Reorder linking and optimizations | Martin 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-02 | CMake: check for ctype and mallinfo functions with CXX instead of C compiler | Julian Büning | |
2018-06-29 | Fix the final -Wimplicit-fallthrough warning | Daniel Schemmel | |
2018-06-29 | Make ConstantExpr hashing function faster and modify affected test | Timotej Kapus | |
2018-06-13 | klee_int: allow NULL as name | Frank Busse | |
2018-06-11 | Fixed memory leak from Executor::inCloseMerge, fixes #883 | Lukas Wölfer | |
2018-05-24 | isLSB should be a boolean, as it is only used in truth contexts | Daniel Schemmel | |
2018-05-24 | remove switch fallthrough in floating point comparision | Daniel Schemmel | |
2018-05-24 | llvm37: handle getRegisteredOptions | Jiri 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-24 | llvm: make KLEE compile against LLVM 3.7 | Richard Trembecký | |
Signed-off-by: Jiri Slaby <jirislaby@gmail.com> | |||
2018-05-24 | llvm37: handle GetElementPtrInst::Create's new parameter | Jiri 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-22 | clang-format on lib/Module/{IntrinsicCleaner.cpp,Passes.h} | Julian Büning | |
2018-05-22 | some housekeeping in Passes.h and IntrinsicCleaner.cpp | Julian 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-22 | CompressionStream: fix sporadic segfaults (uninitialised avail_in) | Frank Busse | |
2018-05-22 | Removed .c_str() from getSourceLocation calls | Cristian Cadar | |
2018-05-22 | Renamed printFileLine to getSourceLocation (as suggested by @delcypher) to ↵ | Cristian Cadar | |
reflect the fact that it simply returns a string | |||
2018-05-22 | Simplified printFileLine by using std::to_string, and removed unneeded ↵ | Cristian Cadar | |
version that takes an argument a stream | |||
2018-05-21 | stop using DEBUG macro name | Jiri 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-21 | fix some casts for LLP64 compilers | Frank Busse | |
2018-05-17 | Abort execution if --only-output-states-covering-new is enabled but its ↵ | Cristian Cadar | |
dependency --output-istats is not | |||
2018-05-17 | Add support for concretizing symbolic objects passed to external functions | Timotej Kapus | |
2018-05-17 | Improve error messages for ReadStringAtAddress | Timotej Kapus | |
2018-05-15 | Improved code quality | Lukas Wölfer | |
2018-05-15 | Implemented incomplete merging | Lukas Wölfer | |
2018-05-15 | remove QueryLog.h | Frank Busse | |
2018-05-09 | Improve handling of constant array in Z3 | Timotej Kapus | |
2018-05-09 | Remove the option for truncating lines in assembly.ll | Martin Nowack | |
The behaviour couldn't be triggered for a kcachegrind from 2012. | |||
2018-05-09 | Remove workaround for bug in older LLVM version (< 3) | Martin Nowack | |
2018-05-09 | Fix include files | Martin Nowack | |
2018-05-05 | Fix handling of errno if external functions are invoked | Martin Nowack | |
If an external function in KLEE is invoked, it might update errno. Previously, the errno specific variable in a state was only updated if it was part of the executed instructions. That opened up a timeframe that increased the likelihood of errno being overwritten by another method call. This patch fixes two issues: * the errno of the KLEE process state is updated before the external function call allowing to detect changes to it later on * after the external call, the memory object of errno is directly updated with its new value, reducing the likelihood to be overwritten by another call Additional features: * Add support for `errno()` for Darwin as well. * Simplified errno handling in POSIX layer | |||
2018-05-05 | Factor out method to update state memory with process state | Martin Nowack | |
2018-05-01 | add blockaddress and indirectbr instructions | Frank Busse | |
2018-05-01 | fix compilation warning | Frank Busse | |
2018-04-09 | doDumpStates: incorrectly increments stats | Frank Busse | |
doDumpStates calls stepInstruction and therefore indirectly increases time and instruction statistics for all dangling (dumped) states. This patch removes the call, but now the timing stats for the last executed state are lost, as StatsTracker::stepInstruction isn't called anymore. | |||
2018-03-01 | Store CexCache stats and then update klee-stats to use them | Domenico Fabio Marino | |
Signed-off-by: Domenico Fabio Marino <nospamdomi@hotmail.it> | |||
2018-02-18 | Fail for aggegrations with big endian ordering | Martin Nowack | |
2018-02-18 | Fixed handling of constant vectors with complex data | Martin Nowack | |
2018-02-18 | Make print function of ObjectState public and const | Martin Nowack | |
2018-02-18 | Fix correct element order of InsertElement/ExtractElement | Martin Nowack | |
2018-02-18 | Fix getelementptr for array or vector indices | Martin Nowack | |
Rewrote code based on: llvm::GEPOperator::accumulateConstantOffset(): Handle signed offset correctly. | |||
2018-02-18 | Fix generation of expressions from constant sequential data | Martin Nowack | |
2018-02-18 | Added comment for getPointerWidth | Martin Nowack | |
2018-02-01 | llvm50: use auto variable instead of SwitchInst::CaseIt | Jiri Slaby | |
llvm50 changed the semantics of SwitchInst::CaseIt and started using "auto" variable type. So use it here too for all versions greater than 3.4 -- 3.4 does not support this semantics yet. Signed-off-by: Jiri Slaby <jirislaby@gmail.com> | |||
2017-11-30 | Implemented bounded merging functionality | Lukas Wölfer | |
2017-11-30 | Added pause and continue functionality for states in Executor | Lukas Wölfer | |
2017-11-24 | klee_make_symbolic: warn on deprecated usage | Frank Busse | |
* terminates state instead of using assertion for illegal argument number * renames empty names to "unnamed" (otherwise test generation fails) * deprecates two argument version | |||
2017-10-25 | fixing huge allocation size constant to be unsigned | David Trabish | |
2017-10-17 | [cmake] detect available metaSMT backends using a pre-defined flag and raise ↵ | Hoang M. Le | |
compile flags accordingly |