-
Notifications
You must be signed in to change notification settings - Fork 478
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
New working model of strlen #1725
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looking good so far!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM. Thank you for the fix!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looking good! Your implementation looks solid to me, but I did leave a couple of questions about why you chose this particular approach.
@ekilmer @ehennenfent I opted to preserve both model strategies and note the difference in them. I'm thinking this is probably the best solution for allowing the most user control over strategies and tradeoffs based on the program being analyzed. |
* master: Create a model for strncpy (#1770) Add doc, fix output bugs (#1769) Update EVM usage example (#1772) New working model of strlen (#1725) Typo (#1768) Specialized iterative serialization for Array (#1756) Enable nightly uploads to PyPI (#1757) Manticore 0.3.4 (#1720) Manticore verifier (#1717) Nightly MacOS Tests (#1614) Remove/procrastinate solver query in ether leak detector (#1727) Fix constant folding & constraint set slicing (#1706)
Updates to the strlen model based on work from strcpy. It seems to be working on concrete and symbolic values. The symbolic testing for strlen will need to be updated.