Skip to content

Make guard_exprt::operator-= work with individual conditions #5753

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
merged 1 commit into from
Jan 16, 2021

Conversation

tautschnig
Copy link
Collaborator

Before, operator-= would only apply when both of the operands were
conjunctions. Yet it is perfectly safe use when one or both operands
aren't conjunctions.

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

Before, operator-= would only apply when both of the operands were
conjunctions. Yet it is perfectly safe use when one or both operands
aren't conjunctions.
@codecov
Copy link

codecov bot commented Jan 15, 2021

Codecov Report

Merging #5753 (b899cb0) into develop (786f7d7) will increase coverage by 0.00%.
The diff coverage is 91.66%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5753   +/-   ##
========================================
  Coverage    69.62%   69.63%           
========================================
  Files         1243     1243           
  Lines       100812   100823   +11     
========================================
+ Hits         70194    70207   +13     
+ Misses       30618    30616    -2     
Flag Coverage Δ
cproversmt2 43.36% <50.00%> (+<0.01%) ⬆️
regression 66.54% <91.66%> (+<0.01%) ⬆️
unit 32.21% <0.00%> (-0.01%) ⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
src/analyses/guard_expr.cpp 98.50% <91.66%> (-1.50%) ⬇️
src/goto-symex/show_program.cpp 91.73% <0.00%> (+2.47%) ⬆️

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 786f7d7...b899cb0. Read the comment docs.

Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

Obviously I wonder "could this go further" but I think the point is to keep it light weight. The BDD patches et al. are probably a better solution than much more explicit case-by-case handling.

@tautschnig tautschnig merged commit 0246e3d into diffblue:develop Jan 16, 2021
@tautschnig tautschnig deleted the guard-simpl branch January 16, 2021 22:05
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