about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2020-07-29remove holes in Instruction-/FunctionInfoTable, add documentationFrank Busse
2020-07-01Clean-up and add documentationMartin Nowack
2020-07-01Remove state contructor with constraintsMartin Nowack
This constructor has been a hack and was wrongly used, use ConstraintManager instead. Allow copy-constructing states only via `ExecutionState::branch()` call.
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-01Use `unique_ptr` for solver in timing solverMartin Nowack
2020-07-01Separate constraint set and constraint managerMartin Nowack
2020-07-01Move constraint implementation from header to cpp filesMartin Nowack
2020-06-29Enable subsets for RandomPathSearcherTimotej Kapus
2020-06-29[PTree] Replace left/right with PointerIntPairTimotej Kapus
2020-06-29Revert "refactor PTree: use unique_ptr"Timotej Kapus
This reverts commit 0aed7731210d0eb41c0ea767edb8067130cf6252.
2020-06-29Implement fshr/fshl intrinsicsAlastair Reid
Changes: - IntrinsicCleaner accepts fshr/fshl as accepted intrinsics - Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract - Klee/main suppresses warnings about externals that are LLVM reserved (i.e., begin with "llvm.") - New test exercises 32 and 7 bit versions including oversize shift values Test values are based on LLVM's test for fshl/fshr - Changes that depend on existence of fshr/fshl are guarded by #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) or ; REQUIRES: geq-llvm-7.0
2020-06-26[FreeBSD] Assume always yes for installing packages as wellMartin Nowack
2020-06-26Switch to a more recent version of SQLite in the CICristian Cadar
2020-06-26Revert to FreeBSD 12.1-STABLE (13.0-CURRENT has started running into issues)Cristian Cadar
2020-06-25Enforce fork/branch limits in branch() and fix double terminationFrank Busse
* extend help messages for -max-memory and -max-memory-inhibit * introduces branchingPermitted() * enforces fork/branch limits in branch() (vector version) * changes main loop * calls updateStates() before checkMemoryUsage() * calls updateStates() again in case we early terminate states This should prevent double termination for now. Other solutions are imho more expensive as we would have to compare possibly large vectors of states (either states(arr) in checkMemoryUsage() or removedStates in terminateState()).
2020-06-25fix Executor: initializeGlobalAliasesJulian Büning
2020-06-25Executor: consolidate initialization of global objectsJulian Büning
2020-06-25Executor: light refactoring of {allocate,initialize}GlobalObjectsJulian Büning
mainly range-based for, code deduplication
2020-06-25Executor: split initializeGlobalsJulian Büning
2020-06-25ExecutorUtil: assert that GlobalValue is already knownJulian Büning
2020-06-25add simple unknown bitcast alias test from the original issueJulian Büning
2020-06-25add known bitcast test for comparisonJulian Büning
2020-06-25regression test for unknown bitcast aliasJulian Büning
2020-06-24StatsTracker: initialize indexed stats when user searcher requires MD2UAdrian Herrera
This is the same check used in Executor::setModule. Without this check, KLEE will segfault in StatisticsManager::incrementIndexedValue, getIndexedValue, and setIndexedValue when `-output-stats=false` or `-output-istats=false` because StatisticsManager::indexedStats has not been allocated.
2020-06-24print stateID with --debug-print-instructionsFrank Busse
2020-06-24add ExecutionState IDsFrank Busse
* add getID()/setID() * use ExecutionStateIDCompare in Executor::states set * output state id in .err files
2020-06-24slightly update ExecutionState, remove holes in structFrank Busse
2020-06-19Added test reported in https://github.com/klee/klee/issues/189 for byval ↵Cristian Cadar
variadic arguments
2020-06-19Renamed Vararg.c to VarArg.c for consistency with the other var arg tests ↵Cristian Cadar
and reformatted comments.
2020-06-19Added test checking for correct alignment of variadic argumentsCristian Cadar
2020-06-19Correctly copy variadic arguments with byval attributeCristian Cadar
2020-06-19Renamed loop index from "i" to "k" in executeCall() so that we can reuse ↵Cristian Cadar
"Instruction *i" declared at the beginning of the function. Reformatted this function.
2020-06-19Added test checking that KLEE correctly handles variadic arguments with the ↵Cristian Cadar
byval attribute
2020-06-17remove cmake warningFrank Busse
* rename SQLITE3 to SQLite3 CMake Warning (dev) at /usr/share/cmake-3.17/Modules/FindPackageHandleStandardArgs.cmake:272 (message): The package name passed to `find_package_handle_standard_args` (SQLITE3) does not match the name of the calling package (SQLite3). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): cmake/modules/FindSQLite3.cmake:26 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) CMakeLists.txt:430 (find_package) This warning is for project developers. Use -Wno-dev to suppress it.
2020-06-06[Module] Add testcase for inline asm liftingMartin Nowack
2020-06-06[Module] Disable lifting for inline asm resembling memory fences with return ↵Martin Nowack
values Inline asm used for memory barriers might use their operands and propagate them as return value. This is currently not supported. Tighten check for this condition and do not to lift those inline asm instructions. Fixes #1252
2020-05-01Add test case from #1257 to reproduce behaviourMartin Nowack
2020-05-01[Solver:STP] Fix handling of array namesMartin Nowack
Array names used for STP queries used to be restricted to 32 characters, with the last characters replaced by a unique number. Similarly, an array is made unique by `klee_make_symbolic`. Unfortunately, both combined can lead to the generation of the same STP array name for different arrays. This leads to wrong queries with invalid results. This is more likely be triggered with longer names for `klee_make_symbolic` Fixes #1257
2020-04-30docker: install KLEE headers in system include pathXiao Liang
Co-authored with @MartinNowack
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-20Consistently define variable using notation VAR=value; fixed comment placementCristian Cadar
2020-04-20Named jobs in Travis CI for better visualization of resultsCristian Cadar
2020-04-09[posix-runtime] Improve model to handle full-path symbolic filesTimotej Kapus
2020-04-09[posix-runtime] Add test for full path consistency for symbolic filesTimotej Kapus
2020-04-08readStringAtAddress: support pointer into objectsMarek Chalupa
The code assumed that the passed pointer points at the beginning of the object. Remove this assumption and support any (constant) pointer. The string is read util either the end of the object is hit (in which case a warning is issued as the string was not zero terminated) or until the terminating zero is found.
2020-04-08test: add a new test for readStringAtAddressMarek Chalupa
Read strings from different parts of objects.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 21:29:43 +0000