Skip to content
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

Fix ENABLE_ARRAY_FIELD_SENSITIVITY #7827

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from

Conversation

peterschrammel
Copy link
Member

Turning off that switch would lead to compilation errors, which are now fixed.

  • 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/
  • [n/a] 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.

Turning off that switch would lead to compilation errors,
which are now fixed.
@peterschrammel peterschrammel force-pushed the ps/fix-array-sensitivity-switch branch from 500f664 to 3381e08 Compare July 26, 2023 17:45
@codecov
Copy link

codecov bot commented Jul 26, 2023

Codecov Report

Patch coverage: 100.00% and project coverage change: +0.10% 🎉

Comparison is base (cdea666) 78.38% compared to head (3381e08) 78.49%.

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #7827      +/-   ##
===========================================
+ Coverage    78.38%   78.49%   +0.10%     
===========================================
  Files         1698     1698              
  Lines       194123   194123              
===========================================
+ Hits        152160   152371     +211     
+ Misses       41963    41752     -211     
Files Changed Coverage Δ
src/goto-symex/field_sensitivity.cpp 92.69% <ø> (ø)
src/goto-symex/field_sensitivity.h 100.00% <100.00%> (ø)

... and 45 files with indirect coverage changes

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

@tautschnig
Copy link
Collaborator

I'd prefer to instead get rid of this #define and just leave it as a feature that can be disabled at runtime (via --max-field-sensitivity-array-size 0).

@tautschnig
Copy link
Collaborator

I'd prefer to instead get rid of this #define and just leave it as a feature that can be disabled at runtime (via --max-field-sensitivity-array-size 0).

We even have --no-array-field-sensitivity as I just realised (which in turn is equivalent to using --max-field-sensitivity-array-size 0). So I maintain that we just just leave it with that runtime option and get rid of the #define.

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.

2 participants