Open
Conversation
Simple combination of heap and interval domains. New domain is created that contains both domains together. Heap domain is used for pointer variables and interval domain is used for numerical variables.
Only pointers to structures were considered so far.
Also add some missing checks for existing location in the SSA heap analysis.
Add working tests for SLL to DLL transformation.
Add comments for methods and important unclear parts. Improve code formatting following cpplint. Remove auto keyword where reasonable and transform iterator-based loops to for-ranged loops.
Use new binary and add assertion to dll1_simple.
Tests for the merge of heap branch used old 2ls binary, so some merge errors were overlooked. Now both heap tests work.
Remove unnecessary includes and use <...> for includes from other directories. Use #if 0 to commented code.
Follow instructions in comments for the PR.
…pointer object. Instead of working with identifier string and stripping away 'obj suffix, we create an utility function for getting identifier of pointed objects in ssa_pointed_objects.
… address of something different than a symbol. Instead, we consider this as nondeterministic value. Fixes diffblue#2.
If both domains return True, result is just True, not True && True. Also improve filtering of variables.
and remove buggy linter rules
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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.
Current implementation for disjunctive domains.
Things that are implemented:
i) Templates corresponding to the current elaboration
ii) SSA corresponding to current elaboration
Things that don't work properly or are incorrect so far:
i) There's a bug that causes the program to crash when generating post constraints (strategy_solver_disjunctive.cpp:592). The rest of the binary search algorithm has to be implemented.
ii) Current post computation doesn't use different values for pre and post. Also, the loop select guard has to be set to true for all post computation except for the initial one.
iii) Guards for the loopheads for each replication are currently left free