about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2024-05-02Refine support for stdio capture psychicNguyễn Gia Phong
2024-03-05Relax revision combination checkNguyễn Gia Phong
2024-03-05Hack up brute-force decision tree constructionNguyễn Gia Phong
2024-03-05Clean up interfacesNguyễn Gia Phong
Psychic now extract patch number directly from meta conditions. Previously it was under the assumption that a patch is triggered by multiple choices. Now we allow a patch to have multiple hunks and the possibility to combine multiple patches. Internally, the code relevant diff test generation is moved under Differentiator.
2024-03-05Revert orphaned changesNguyễn Gia Phong
2024-03-05Handle conjoined metaconstraintsNguyễn Gia Phong
2024-03-05Move differentiator to separate moduleNguyễn Gia Phong
2024-03-05Execute concrete programs more eagerlyNguyễn Gia Phong
2024-03-05Implement detection of implicit return via pointerNguyễn Gia Phong
2024-03-05Implement return value detectionNguyễn Gia Phong
Values returned after reaching patch location from functions in the specified source file are now automatically accounted for differential test generation.
2024-03-05Handle revisited meta sym var when generate env varNguyễn Gia Phong
I still have no clue in some cases why they are seen more than once.
2024-03-05Retire external symbilic diffNguyễn Gia Phong
2024-03-05Implement native path condition combinationNguyễn Gia Phong
2024-03-05Fix metavar detection false negativeNguyễn Gia Phong
2024-03-05Port seeding wrapper to KLEE 3Nguyễn Gia Phong
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)
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-05-20 06:05:41 +0000