about summary refs log tree commit diff homepage
path: root/include
AgeCommit message (Collapse)Author
2022-04-28Make Uclibc support a runtime option, not a compile-time one.Gleb Popov
2022-04-25use mallinfo2 if availableFrank Busse
2022-03-17remove obsolete KLEE_LLVM legacy definesJulian Büning
2022-03-17ADT/Ref.h: remove headerFrank Busse
2022-03-17remove LLVM < 6 from sourcesFrank Busse
2022-03-17Document that GetTotalMallocUsage returns the usage in bytesCristian Cadar
2022-01-05introduce BranchTypesFrank Busse
2021-12-23Introduce termination categoriesFrank Busse
Track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated.
2021-05-04differentiate between partial and completed paths in summary and fix paths ↵Frank Busse
stats when not dumping states
2020-12-23klee.h: fix compiler warnings (function declaration is not a prototype)Frank Busse
2020-11-12Casting.h: isa_and_nonnull<>Julian Büning
2020-11-12Ref: implement operator bool()Julian Büning
2020-11-04Link to the different runtime libraries depending on the application to test.Martin Nowack
Currently, only 32bit vs. 64bit is supported.
2020-10-12Exception handling only for LLVM >= 8.0.0Julian Büning
2020-09-26Replace llvm::CallSite with llvm::CallBase on LLVM 8+Lukas Zaoral
This is in preparation for LLVM 11 as the llvm:CallSite class has been removed.
2020-08-19DiscretePDF: use IDs instead of pointers (see PR #739)Frank Busse
2020-08-07New intrinsic: klee_is_replayAlastair Reid
This instrinsic detects whether the program is being executed symbolically or concretely (i.e., using the libkleeRuntest library). The intended usage (illustrated in the test program) is to allow the test program to display the input values by invoking any libraries it wants to. This is especially valuable if you are constructing complex, structured values and for languages like Rust (or C++) that have rich libraries and print libraries. For example, you might pick a symbolic value N with the assumption "0 <= N < 10" and then pick N symbolic values and write them to an array. The resulting ktest file is a bit hard to understand compared with the output of the standard print function in Rust/C++.
2020-07-30introduce --rng-initial-seed=<unsigned>Frank Busse
* move global theRNG into Executor * pass theRNG via ctor to searchers * remove some type warnings from RNG.cpp Fixes #1023.
2020-07-29remove holes in Instruction-/FunctionInfoTable, add documentationFrank Busse
2020-07-01Clean-up and add documentationMartin Nowack
2020-07-01Use constraint sets and separate metadata for timing solver invocationMartin Nowack
Decouple ExecutionState from TimingSolver Instead of providing an execution state to the timing solver use a set of constraints and an additional object for metadata. Fixes: * correct accounting of metadata to a specific state * accounting of all solver invocations (e.g. solver-getRange was not accounted) * allows to invoke the solver without a state (avoids costly copying of states/constraints)
2020-07-01Separate constraint set and constraint managerMartin Nowack
2020-07-01Move constraint implementation from header to cpp filesMartin Nowack
2020-04-30Moved header files that were placed directly in include/klee/ into ↵Cristian Cadar
appropriate existing directories and a new directory Statistics; a few missing renames.
2020-04-30Removed include/klee/util and moved header files to appropriate placesCristian Cadar
2020-04-30Created include/klee/Core directory and moved appropriate files direc\Cristian Cadar
tly in lib/Core
2020-04-30Move header files from lib/Expr to include/klee/Expr to eliminate includes ↵Cristian Cadar
using "../"
2020-04-30Removed the Internal directory from include/kleeCristian Cadar
2020-04-08Statistic: slightly modernise class definitionFrank Busse
2020-04-08stats: remove queryConstructTime (unused)Frank Busse
2020-02-19Use `ref<>` for MemoryObject handlingMartin Nowack
This uses the `ref<>`-based memory handling of MemoryObjects. This makes it explicit that references are held in: - ExecutionState::symbolics - ObjectState
2020-02-19Use `ref<>` for UpdateNodeMartin Nowack
Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code.
2020-02-19Clean-up header filesMartin Nowack
* Replace c header with c++ header * remove unneeded header file
2020-02-19Add move assignment operator and move construct for `ref` class.Martin Nowack
2020-02-19Add `ReferenceCounter` struct utilized by ref<>Martin Nowack
Using KLEE's `ref<>` shared ptr requires the referenced object to contain a reference counter to be added and initialised to 0 as part of the constructor. To support better reuse of the `ref<>` ptr add a `ReferenceCounter` struct. Just adding this struct to a new class/struct as member enables reference counting with `ref<>` - no additional counter management needed.
2020-02-19Fix ptr reference invalidation if last reference gets freed before new ↵Martin Nowack
reference assigned.
2020-02-13Use call-by-reference for hash-function invocationMartin Nowack
2020-02-13Replace old TR1 implementations of unordered_map/set with std::* versionsMartin Nowack
TR1 implementation got replaced by the std::* equivalents with C++11. Start to use the standard versions instead of the old ones.
2019-12-12[Searchers] Remove weight from es, add nurs_depthTimotej Kapus
Having both weight and depth in execution state is wasteful, therefore this patch removes weight. The nurs:depth searcher is replaced by nurs:rp, which uses pow to compute the weight A new nurs:depth searcher is introduced that biases the search with depth, making it the only other searcher that prefers to go deep (similar to dfs).
2019-11-28Move merging related code from Executor into MergingSearcherLukas Wölfer
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de>
2019-11-07[expr-visitor] Remove unnecessary allocationTimotej Kapus
2019-10-29ExecutorTimers: refactor and move to support libFrank 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-09-03Moved solver-related header files into a separate klee/Solver/ directory.Cristian Cadar
2019-07-30Use #include "klee/..." (instead of #include <klee/...>) consistently.Cristian Cadar
2019-07-30Consolidated 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-23Refactor ConstraintManager to more modern coding standardsDaniel Schemmel
Eliminates -Wdeprecated-copy warnings Performed clang-format on touched file
2019-06-04fix some incorrect first linesJulian Büning
2019-06-04make endif guard naming consistentJulian Büning
2019-06-04DiscretePdf.h: add include guardsJulian Büning
2019-06-04make include guard naming consistentJulian Büning