Skip to content
This repository was archived by the owner on Jun 24, 2026. It is now read-only.

New working model of strlen#1725

Merged
sschriner merged 11 commits into
masterfrom
c_strlen_dev
Jul 7, 2020
Merged

New working model of strlen#1725
sschriner merged 11 commits into
masterfrom
c_strlen_dev

Conversation

@sschriner

Copy link
Copy Markdown
Contributor

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.

@sschriner
sschriner requested review from ekilmer and woodruffw June 11, 2020 17:51
@sschriner sschriner self-assigned this Jun 11, 2020

@ekilmer ekilmer left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking good so far!

Comment thread tests/native/test_models.py Outdated
@sschriner
sschriner requested a review from ekilmer June 12, 2020 15:24
@sschriner
sschriner marked this pull request as ready for review June 17, 2020 14:48

@ekilmer ekilmer left a comment

Copy link
Copy Markdown
Contributor

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!

@ehennenfent ehennenfent linked an issue Jun 22, 2020 that may be closed by this pull request

@ehennenfent ehennenfent left a comment

Copy link
Copy Markdown
Contributor

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.

Comment thread manticore/native/models.py Outdated
Comment thread manticore/native/models.py
Comment thread manticore/native/models.py
@sschriner

Copy link
Copy Markdown
Contributor Author

@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.

@sschriner
sschriner merged commit 14ef9ec into master Jul 7, 2020
@sschriner
sschriner deleted the c_strlen_dev branch July 7, 2020 17:25
ekilmer added a commit that referenced this pull request Jul 17, 2020
* 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)
@ehennenfent ehennenfent added this to the Manticore 0.3.5 milestone Sep 3, 2020
@ehennenfent ehennenfent mentioned this pull request Oct 6, 2020
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Add a model for Strlen

3 participants