Merge lazy init by Jakub Novák #22
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ASan report: include/klee/util/BitArray.h:44:74: runtime error: null pointer passed as argument 1, which is declared to never be null Signed-off-by: Marek Chalupa <xchalup4@fi.muni.cz>
ASan report: include/klee/util/BitArray.h:32:54: runtime error: null pointer passed as argument 2, which is declared to never be null Signed-off-by: Marek Chalupa <xchalup4@fi.muni.cz>
lib/Core/Executor.cpp:4077:3: runtime error: load of value 30, which is not a valid value for type 'bool' Fixes: 95fe47d
…pdates() Fixes: /usr/include/c++/12.1.0/bits/stl_vector.h:1124:34: runtime error: reference binding to null pointer of type 'struct value_type' 0 0x55f1e36d289b in std::vector<klee::ref<klee::ConstantExpr>, std::allocator<klee::ref<klee::ConstantExpr> > >::operator[](unsigned long) /usr/include/c++/12.1.0/bits/stl_vector.h:1124 1 0x55f1e36c1725 in klee::ObjectStatePlane::getUpdates() const lib/Core/Memory.cpp:161
JetKlee Lazy Init rebased for llvm 14
…KleeLazyInitMerge # Conflicts: # lib/Core/Executor.cpp
Prefix all of them with 'memory error:'.
We over-approximate, but the models should be good enough for most purposes.
It has side-effects that we do not support yet.
It's like gettext.
It is not passing for now
Functions are not sized types, therefore llvm crashed on this call.
Previously, two separate data structures were used for the same thing. This fixes the issue and also fixes multiple writes into the same offset in an array
if parent was local, be local. If it was global, also be global
lazy objects inherit scope of parent
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This pull request adds lazy init functionality by Jakub Novák.
It also rebases JetKlee to the upstream version of Klee (at the time of the creation of the branch).