Skip to content

make_byte_{extract,update} to build byte_{extract,update} expressions #6056

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
May 6, 2021

Conversation

tautschnig
Copy link
Collaborator

Remove byte_{extract,update}id from the API (marking them static) and
instead add factory functions make_byte
{extract,update} to construct
the full expression. These functions will ensure that both endianness
and byte width are consistently configured.

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

Remove byte_{extract,update}_id from the API (marking them static) and
instead add factory functions make_byte_{extract,update} to construct
the full expression. These functions will ensure that both endianness
and byte width are consistently configured.
@tautschnig tautschnig removed their assignment Apr 23, 2021
@codecov
Copy link

codecov bot commented Apr 23, 2021

Codecov Report

Merging #6056 (e7d8209) into develop (ff5902e) will increase coverage by 0.01%.
The diff coverage is 87.37%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6056      +/-   ##
===========================================
+ Coverage    74.25%   74.27%   +0.01%     
===========================================
  Files         1444     1444              
  Lines       157460   157436      -24     
===========================================
+ Hits        116928   116930       +2     
+ Misses       40532    40506      -26     
Impacted Files Coverage Δ
src/goto-instrument/code_contracts.h 94.11% <ø> (ø)
src/solvers/flattening/boolbv.cpp 80.00% <0.00%> (+0.47%) ⬆️
src/solvers/flattening/boolbv_case.cpp 0.00% <0.00%> (ø)
src/solvers/flattening/boolbv_cond.cpp 0.00% <0.00%> (ø)
src/solvers/prop/prop.cpp 42.85% <0.00%> (-42.86%) ⬇️
src/solvers/prop/prop.h 84.37% <ø> (ø)
src/solvers/sat/cnf.h 83.33% <ø> (ø)
src/util/byte_operators.h 90.24% <ø> (-9.76%) ⬇️
unit/util/pointer_offset_size.cpp 100.00% <ø> (ø)
src/goto-symex/symex_dereference.cpp 89.83% <66.66%> (+0.47%) ⬆️
... and 51 more

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 4a7b064...e7d8209. Read the comment docs.

array_typet(unsignedbv_typet(8),
from_integer(bytes_req, offset.type())));
array_typet(
unsignedbv_typet(8), from_integer(bytes_req, offset.type())));
Copy link
Contributor

Choose a reason for hiding this comment

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

I know this a refactor, but can we replace the 8 with something less magic?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

#917, which this PR is supposed to make easier to merge :-)

@tautschnig tautschnig merged commit 56adbb2 into diffblue:develop May 6, 2021
@tautschnig tautschnig deleted the make_byte_X branch May 6, 2021 20:31
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.

4 participants