about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2024-03-05Fallback on UBNguyễn Gia Phong
This is not benefitting off UBSan, but there are too many moving parts now that a common denominator is needed for me to mentally keep track of things. (Yes, it's embarrassing that I commit less often working on software engineering research software, now I'm paying the price.)-;
2024-03-05Support 1-byte metavariablesNguyễn Gia Phong
2024-03-05Make symbolic stdout more flexibleNguyễn Gia Phong
2024-03-05Add search heuristic for patch locationsNguyễn Gia Phong
2024-03-05Avoid resolving combined SMT formulaeNguyễn Gia Phong
2024-03-05Half-bake decision clusteringNguyễn Gia Phong
2024-03-05Conclude concrete execution implNguyễn Gia Phong
2024-03-05Lay ground work for concrete executionNguyễn Gia Phong
2024-03-05Clone state more completelyNguyễn Gia Phong
2024-03-05Implement differentiator extractionNguyễn Gia Phong
2024-03-05Save exited states' formulaNguyễn Gia Phong
2024-03-05Receive instrumented revision numberNguyễn Gia Phong
2024-03-05Implement differencial test structureNguyễn Gia Phong
2024-02-29Final changes to release notes for v3.1Cristian Cadar
2024-02-29Add support to fully concretise objects if modified externallyMartin Nowack
Propagate ExternalCallPolicy to allow user-based selection.
2024-02-29Support external call concretisation policies for referenced objectsMartin Nowack
Provide an additional argument to select the concretisation policy. Fix a bug where the concretisation of a shared memory object was visible across different states by retrieving a writable object state first.
2024-02-29Refactor `ObjectState::flushToConcreteStore` to use `toConstant`Martin Nowack
Use existing `Executor::toConstant()` function to transform a symbolic byte of an `ObjectState` to its concrete representation. This will also add constraints if required.
2024-02-29Use correctly constrained constants if the memory object is fully symbolicMartin Nowack
Before, only partially symbolic variables have been concretized. Now, every object that is not fully concrete is concretized correctly this includes fully symbolic objects.
2024-02-29Correctly update symbolic variables that have been changed externallyMartin Nowack
Before, external changes to symbolic variables have not been propagated back to their internal representation. Do a byte-by-byte comparison and update object state if required.
2024-02-29Test case for externally concretized variables and constraint fully symbolic ↵Martin Nowack
variables The test case is based on the example provided by Mingyi Liu from the KLEE mailing list.
2024-02-29Release notes for KLEE 3.1Cristian Cadar
2024-02-29Set version number to 3.1Cristian Cadar
2024-02-28Compare LLVM_VERSION_SHORT to "140" rather than "14".Michael Herstine
In commit 2b07721, support was added to p-libcxx.inc & p-llvm.inc for LLVM versions 14+ (in which, apparently, certain build flags were changed). To detect these recent versions, the variable LLVM_VERSION_SHORT was compared numerically to "14"-- the intent obviously being to express "LLVM version 14 or later". However, in both v-clang.inc & v-llvm.inc, LLVM_VERSION_SHORT is defined as the concatenation of LLVM_VERSION_MAJOR and LLVM_VERSION_MINOR. Therefore, on a machine with, say, LLVM 13.0 installed, LLVM_VERSION_SHORT will be "130" which compares as larger than "14". This patch changes the comparison to be against "140".
2024-02-27Small refactorings and reformatting in callExternalFunctionCristian Cadar
2024-02-27Simplified callExternalFunction by using toConstant instead of getValueCristian Cadar
2024-02-27Extend toConstant() to take an additional boolean argument that decides ↵Cristian Cadar
whether the expression is concretised. Also changed a C string argument to std::string.
2024-02-27This commit fixes the concretization of arguments following an external call ↵Cristian Cadar
with symbolic arguments. It also introduces a new external call policy, where the symbolic inputs are left unconstrained following such a call, useful for certain external calls such as printf.
2024-02-27Two test cases exercising two policies for calling external calls with ↵Cristian Cadar
symbolic arguments. One of them is currently expected to fail.
2024-02-19Rename --ptree-batch-size to --exec-tree-batch size, and ↵Cristian Cadar
--compress-execution-tree to --compress-exec-tree. Fix an incorrect reference to --write-exec-tree.
2024-02-17Remove the not Darwin requirement for the test TargetMismatch.cCristian Cadar
2024-02-17Fixed incorrect reference in ExternalCallWarningsCristian Cadar
2024-02-16drop llvm 9 and 10Daniel Schemmel
2024-02-12Fix brittleness in Feature/VarArgByVal testDaniel Schemmel
2024-02-08Add space between include and main function for updated test casesMartinNowack
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com> (cherry picked from commit 1ea1a7576300a4da01d925df42db109660ef54d2)
2024-02-08Mention default value in help text for `--strip-all` and `--strip-debug`MartinNowack
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com> (cherry picked from commit 5d61fb6114bafbf67c59899d15e397684d4ceb28)
2024-02-08Use `std::` namespace for `uint64_t`MartinNowack
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com> (cherry picked from commit 5d9af025ee5a01b1650f11ed0612a10357a98308)
2024-02-08Enable CI to test newer LLVM versionsMartin Nowack
2024-02-08Support newer LLVM versions in `lit`Martin Nowack
2024-02-08Update test case for expressions using `udiv`, `urem`, `sdiv` and `srem`Martin Nowack
They are not supported anymore for newer LLVM versions.
2024-02-08Handle check for thrown libc++ exceptions more generalMartin Nowack
The wording changed slightly in newer versions. Update the test case to support this.
2024-02-08Disable `2018-10-30-llvm-pr39177.ll` for newer LLVM versions.Martin Nowack
The optimiser generates different code and calls fwrite directly instead.
2024-02-08Disable unsupported passes for newer LLVM versionsMartin Nowack
Similar functionality needs to be added using a new pass manager
2024-02-08Add support to `aligned_alloc` generated by LLVMMartin Nowack
Handle like `memalign` for now.
2024-02-08Add support for `Intrinsic::get_rounding` for LLVM 16Martin Nowack
`Intrinsic::flt_rounds` got removed
2024-02-08Use APIs of newer LLVM versions instead of unsupported onesMartin Nowack
2024-02-08Fix test case: using unsupported `CHECK_NEXT` instead of `CHECK-NEXT`Martin Nowack
2024-02-08Fix test cases to support opaque pointersMartin Nowack
2024-02-08Add support for opaque pointersMartin Nowack
2024-02-08Explicitly enable opaque pointer support for LLVM 15Martin Nowack
This automatically lifts old-style pointers to opaque pointers. More recent versions use opaque pointers automatically and do not need an explicit enabling.
2024-02-08Explicitly build KLEE's exception handling runtime with C++11Martin Nowack
Currently, we assume C++11 support being used to by the tested software. This needs to change if newer C++ standards should be supported.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2026-01-04 10:38:39 +0000