Skip to content

Make going_to variable cprover-prefixed #8312

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

Conversation

qinheping
Copy link
Collaborator

The goint_go variables are cprover variables and hence should be cprover-prefixed.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • 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).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@qinheping qinheping force-pushed the bugfixes/make_going_var_cprover_prefixed branch from fe8bed7 to f993f8c Compare June 5, 2024 04:13
Copy link

codecov bot commented Jun 5, 2024

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 78.29%. Comparing base (52c3dbb) to head (f993f8c).

Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #8312   +/-   ##
========================================
  Coverage    78.29%   78.29%           
========================================
  Files         1722     1722           
  Lines       188448   188448           
  Branches     18464    18452   -12     
========================================
  Hits        147540   147540           
  Misses       40908    40908           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

Please also update src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp

@tautschnig tautschnig merged commit 621fe05 into diffblue:develop Jun 5, 2024
39 of 40 checks passed
@martin-cs
Copy link
Collaborator

Should it also go into linking/remove_internal_symbols.cpp ? More generally, what is the procedure for adding a CPROVER_PREFIX symbol? Do we have a list anywhere of all of them like goto-programs/system_library_symbols.cpp?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants