ToString support for abstract collection using makeSymbolic #391 #402
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.
Description
ToString for lists (as well as for other inheritors of
AbstractCollection
didn't work since it's too complicated for the engine because of StringBuilder usage somewhere inside of it. I've decided to make a temporary solution, implementing this method withmakeSymbolic
mechanism -- the method should return an unbounded symbolic variable, that will allow us to continue the analysis (in contrast to theexecuteConcretely
). Later, the concrete execution will find the right result for such execution, if it's required.My suggestion is based on thoughts that people usually use
toString
on collections just for logging, showing or something like that, and the resulting line won't present in the path constraints. It's not 100% true, but in many cases, it will work.Fixes #391
Type of Change
toString
without concrete executor works differently now for the inheritors of theAbstractCollection
andHashSet
How Has This Been Tested?
Automated Testing
Added test in the corresponding package.
Manual Scenario
Same test, since it is only about
toString
method on any collection.Checklist: