about summary refs log tree commit diff homepage
path: root/include
AgeCommit message (Collapse)Author
2018-10-04config.h.cmin: remove obsolete cmakedefineJulian Büning
2018-09-18llvm4: PointerType is not SequentialTypeJiri Slaby
So handle the type specially whenever needed. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-18llvm4: use chrono helpers from LLVMJiri Slaby
LLVM 4 removes the old time interface and starts using the C++11's chrono. So switch to that in klee for LLVM 4 too. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-06Fix missing includes and declarationsMartin Nowack
2018-07-04Fix uninitialized memory: enums have to be initializedMartin 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-06-29Explicitly initialize value to squelch a potentially uninitialized value warningDaniel Schemmel
2018-06-14Add unittest for DiscretePDFMartin Nowack
2018-06-13klee_int: allow NULL as nameFrank Busse
2018-06-11Fixed memory leak from Executor::inCloseMerge, fixes #883Lukas Wölfer
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-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-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-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-01-22MergeHandler: remove unused closedStateCountJiri Slaby
clang 5 reports: In file included from ../lib/Core/MergeHandler.cpp:10: ../include/klee/MergeHandler.h:81:12: warning: private field 'closedStateCount' is not used [-Wunused-private-field] unsigned closedStateCount; ^ So fix it by removing the member. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-01-08[NFC] Remove unused config header template that was only used byDan Liew
the old build system (now removed).
2017-11-30Implemented bounded merging functionalityLukas Wölfer
2017-10-17add support for CVC4 and Yices2 via metaSMTHoang M. Le
2017-09-22Merge pull request #748 from ccadar/optionsCristian Cadar
Added support for hiding command-line options
2017-08-27Remove unnecessary null pointer checksOscar Deits
Fixes klee/klee#717 delete on null pointer is always safe.
2017-08-11Added support for hiding command-line optionsCristian Cadar
2017-08-04Removed merging searchersLukas Wölfer
2017-07-29Added another variant of printFileLine in KInstruction that returns the ↵Cristian Cadar
location as a string. Also added const qualifier to the printFileLine functions
2017-07-26Now that LLVM 2.9 is gone, we can use cl::bits instead of cl::listCristian Cadar
2017-07-25Added the const qualifier to the keys in the constantMapCristian Cadar
2017-07-23Remove support for LLVM < 3.4Martin Nowack
Request LLVM 3.4 as minimal requirement for KLEE
2017-06-16move module loading into external functionJörg Thalheim
- having an explicit function which is defined for multiple llvm versions separately increases readability. - also: error handling was simplified - Personal motivation: being able to use this functionality in unit tests fixes #561 related to #656
2017-06-16llvm37: introduce type for PassManagerJiri Slaby
In LLVM 3.7, PassManager was moved to the legacy:: namespace. Introduce a type for it and use it in the code. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-06-12llvm: don't use clEnumValEnd for LLVM 4.0Jiri Slaby
It became unnecessary when defining options and mainly undefined. So introduce KLEE_LLVM_CL_VAL_END as suggested by @delcypher. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-06-08Merge pull request #675 from ccadar/varargsAndrea Mattavelli
Fixed typos in comments related to vararg support.
2017-06-08Fixed typos in comments related to vararg support.Cristian Cadar
2017-06-02hide backend solver declarations from public includeHoang M. Le
2017-06-02replace handleMetaSMT() with klee::createMetaSMTSolver() and move it into ↵Hoang M. Le
MetaSMTSolver.cpp so that the backend headers only need to be included once there
2017-06-01Refactor file opening code out of `main.cpp` and intoDan Liew
`klee_open_output_file()` function so that it can be used by the Z3Solver.
2017-03-23Add `AssignmentValidatingSolver`. It's purpose is to check any computedDan Liew
assignments against the corresponding `Query` object and check the assignment evaluates correctly. This can be switched on using `-debug-assignment-validating-solver` on the command line.
2017-03-23[WIP] Fix bug where stats would not be updated on early exit caused byDan Liew
finding a bug with the `-exit-on-error` option enabled.
2017-03-03Moved printFileLine() to be part of KInstructionCristian Cadar
2017-02-25llvm: stop using global contextJiri Slaby
It was marked as deprecated long time ago and finally removed in LLVM 3.9. Remove all uses of getGlobalContext and create our own context. Propagate it all over the code then. [v2] use ctx, not C as name Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-23CommandLine: do not copy list in optionIsSetJiri Slaby
Pass the list as reference. Otherwise we can get errors with newer LLVM like: lib/Basic/ConstructSolverChain.cpp:26:19: error: call to deleted constructor of 'llvm::cl::list<QueryLoggingSolverType>' if (optionIsSet(queryLoggingOptions, SOLVER_KQUERY)) { ^~~~~~~~~~~~~~~~~~~ llvm/Support/CommandLine.h:1466:3: note: 'list' has been explicitly marked deleted here list(const list &) = delete; ^ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-21Teach `klee::getDirectCallTarget()` to resolve weak aliases. This isDan Liew
controlled by a new parameter `moduleIsFullyLinked`. When true the linkage type of a weak alias is ignored. It is legal to do this when the module is fully linked because there won't be another function that could override the weak alias. This fixes a previous assertion failure in `klee::getDirectCallTarget()` triggered by the `test/regression/2016-11-24-bitcast-weak-alias.c` test case.
2017-02-14Refactoring code to improve readability by using UINT32/64_C macrosAndrea Mattavelli
2017-02-14Fixed assertion invocation: We were invoking bits64::truncateToNBits with a ↵Andrea Mattavelli
width greater than 64
2017-02-14Added pre/post conditions as assertionsAndrea Mattavelli
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 12:29:23 +0000