about summary refs log tree commit diff homepage
path: root/include
AgeCommit message (Collapse)Author
2018-10-23Added support for KLEE index-based array optimizationAndrea Mattavelli
2018-10-16Small changes to commentsCristian Cadar
2018-10-16Added missing header to SolverCmdLine.h and clang-format itCristian Cadar
2018-10-16Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file is meant ↵Cristian Cadar
to have only solver options.
2018-10-08add support for klee-replay on OSXFrank Busse
* also adds klee-replay as dependency for systemtests
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>
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-29 00:22:34 +0000