about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2018-07-04Fix compiler warnings if assertions are disabledMartin Nowack
2018-07-04Reorder linking and optimizationsMartin 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-02CMake: check for ctype and mallinfo functions with CXX instead of C compilerJulian Büning
2018-06-29Fix the final -Wimplicit-fallthrough warningDaniel Schemmel
2018-06-29Make ConstantExpr hashing function faster and modify affected testTimotej Kapus
2018-06-13klee_int: allow NULL as nameFrank Busse
2018-06-11Fixed memory leak from Executor::inCloseMerge, fixes #883Lukas Wölfer
2018-05-24isLSB should be a boolean, as it is only used in truth contextsDaniel Schemmel
2018-05-24remove switch fallthrough in floating point comparisionDaniel Schemmel
2018-05-24llvm37: handle getRegisteredOptionsJiri 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-24llvm: make KLEE compile against LLVM 3.7Richard Trembecký
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-05-24llvm37: handle GetElementPtrInst::Create's new parameterJiri 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-22clang-format on lib/Module/{IntrinsicCleaner.cpp,Passes.h}Julian Büning
2018-05-22some housekeeping in Passes.h and IntrinsicCleaner.cppJulian 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-22CompressionStream: fix sporadic segfaults (uninitialised avail_in)Frank Busse
2018-05-22Removed .c_str() from getSourceLocation callsCristian Cadar
2018-05-22Renamed printFileLine to getSourceLocation (as suggested by @delcypher) to ↵Cristian Cadar
reflect the fact that it simply returns a string
2018-05-22Simplified printFileLine by using std::to_string, and removed unneeded ↵Cristian Cadar
version that takes an argument a stream
2018-05-21stop using DEBUG macro nameJiri 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-21fix some casts for LLP64 compilersFrank Busse
2018-05-17Abort execution if --only-output-states-covering-new is enabled but its ↵Cristian Cadar
dependency --output-istats is not
2018-05-17Add support for concretizing symbolic objects passed to external functionsTimotej Kapus
2018-05-17Improve error messages for ReadStringAtAddressTimotej Kapus
2018-05-15Improved code qualityLukas Wölfer
2018-05-15Implemented incomplete mergingLukas Wölfer
2018-05-15remove QueryLog.hFrank Busse
2018-05-09Improve handling of constant array in Z3Timotej Kapus
2018-05-09Remove the option for truncating lines in assembly.llMartin Nowack
The behaviour couldn't be triggered for a kcachegrind from 2012.
2018-05-09Remove workaround for bug in older LLVM version (< 3)Martin Nowack
2018-05-09Fix include filesMartin Nowack
2018-05-05Fix handling of errno if external functions are invokedMartin 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-05Factor out method to update state memory with process stateMartin Nowack
2018-05-01add blockaddress and indirectbr instructionsFrank Busse
2018-05-01fix compilation warningFrank Busse
2018-04-09doDumpStates: incorrectly increments statsFrank 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-01Store CexCache stats and then update klee-stats to use themDomenico Fabio Marino
Signed-off-by: Domenico Fabio Marino <nospamdomi@hotmail.it>
2018-02-18Fail for aggegrations with big endian orderingMartin Nowack
2018-02-18Fixed handling of constant vectors with complex dataMartin Nowack
2018-02-18Make print function of ObjectState public and constMartin Nowack
2018-02-18Fix correct element order of InsertElement/ExtractElementMartin Nowack
2018-02-18Fix getelementptr for array or vector indicesMartin Nowack
Rewrote code based on: llvm::GEPOperator::accumulateConstantOffset(): Handle signed offset correctly.
2018-02-18Fix generation of expressions from constant sequential dataMartin Nowack
2018-02-18Added comment for getPointerWidthMartin Nowack
2018-02-01llvm50: use auto variable instead of SwitchInst::CaseItJiri 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-30Implemented bounded merging functionalityLukas Wölfer
2017-11-30Added pause and continue functionality for states in ExecutorLukas Wölfer
2017-11-24klee_make_symbolic: warn on deprecated usageFrank 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-25fixing huge allocation size constant to be unsignedDavid Trabish
2017-10-17[cmake] detect available metaSMT backends using a pre-defined flag and raise ↵Hoang M. Le
compile flags accordingly
2017-10-17add support for CVC4 and Yices2 via metaSMTHoang M. Le
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-21 11:53:34 +0000