Skip to content

goto-symex: do not rely on undocumented find_symbols(expr) behaviour #6726

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

Merged

Conversation

tautschnig
Copy link
Collaborator

L2 re-renaming should not be applied to symbols contained in the type
(array sizes may be symbolic). Some variants of find_symbols exclude
such symbols, when others don't. (Cleanup thereof takes place in another
commit.) Either way, goto-symex should be explicit in what it wants to
process, which is really just the expression and all its operands.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

L2 re-renaming should not be applied to symbols contained in the type
(array sizes may be symbolic). Some variants of find_symbols exclude
such symbols, when others don't. (Cleanup thereof takes place in another
commit.) Either way, goto-symex should be explicit in what it wants to
process, which is really just the expression and all its operands.
@codecov
Copy link

codecov bot commented Mar 14, 2022

Codecov Report

Merging #6726 (f21e9ed) into develop (9053c5f) will increase coverage by 0.00%.
The diff coverage is 100.00%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #6726   +/-   ##
========================================
  Coverage    76.85%   76.85%           
========================================
  Files         1589     1589           
  Lines       183846   183848    +2     
========================================
+ Hits        141289   141291    +2     
  Misses       42557    42557           
Impacted Files Coverage Δ
src/goto-symex/goto_symex_state.cpp 91.71% <100.00%> (+0.04%) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 3f7f5ae...f21e9ed. Read the comment docs.

@kroening
Copy link
Member

There is one further aspect when "finding" symbols: bound symbols. At the very least the comments should say whether they are included or not.

@tautschnig tautschnig merged commit bb08494 into diffblue:develop Mar 25, 2022
@tautschnig tautschnig deleted the cleanup/symex-finding-symbols branch March 25, 2022 21:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants