Skip to content

Pointer-primitive checks should succeed for valid pointers at object bound#7229

Merged
tautschnig merged 1 commit intodiffblue:developfrom
tautschnig:bugfixes/7064-pointer-primitive-check
Oct 17, 2022
Merged

Pointer-primitive checks should succeed for valid pointers at object bound#7229
tautschnig merged 1 commit intodiffblue:developfrom
tautschnig:bugfixes/7064-pointer-primitive-check

Conversation

@tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Oct 10, 2022

The C standard designates the pointer with offset object size (pointing to the first byte outside the object) to be valid. In keeping with this, --pointer-primitive-check should not designate this as invalid (even when reading non-zero bytes from this object is).

Fixes: #7064

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

@tautschnig tautschnig mentioned this pull request Oct 10, 2022
Closed
@tautschnig tautschnig force-pushed the bugfixes/7064-pointer-primitive-check branch 2 times, most recently from 1095c56 to 8fe7fe0 Compare October 10, 2022 14:56
@tautschnig tautschnig requested a review from nwetzler October 10, 2022 15:04
@tautschnig tautschnig force-pushed the bugfixes/7064-pointer-primitive-check branch 2 times, most recently from 854cdf3 to cf19f00 Compare October 10, 2022 19:57
@codecov
Copy link

codecov bot commented Oct 10, 2022 •
edited
Loading

Codecov Report

Base: 77.99% // Head: 77.96% // Decreases project coverage by -0.03% ⚠️

Coverage data is based on head (dc2a3e9) compared to base (99ce20c).
Patch coverage: 100.00% of modified lines in pull request are covered.

❗ Current head dc2a3e9 differs from pull request most recent head 1c03453. Consider uploading reports for the commit 1c03453 to get more accurate results

Additional details and impacted files 
@@             Coverage Diff             @@
##           develop    #7229      +/-   ##
===========================================
- Coverage    77.99%   77.96%   -0.04%     
===========================================
  Files         1619     1616       -3     
  Lines       187184   186813     -371     
===========================================
- Hits        145999   145644     -355     
+ Misses       41185    41169      -16
Impacted Files Coverage Δ
src/ansi-c/goto_check_c.cpp 91.50% <100.00%> (-0.05%) ⬇️
src/crangler/c_defines.cpp 80.00% <0.00%> (-12.00%) ⬇️
src/crangler/ctokenit.cpp 72.41% <0.00%> (-10.35%) ⬇️
src/linking/linking.cpp 69.05% <0.00%> (-3.03%) ⬇️
src/crangler/c_wrangler.cpp 75.51% <0.00%> (-2.44%) ⬇️
src/util/simplify_expr.cpp 83.71% <0.00%> (-0.07%) ⬇️
src/util/source_location.h 100.00% <0.00%> (ø)
src/ansi-c/ansi_c_internal_additions.cpp 90.12% <0.00%> (ø)
...rc/solvers/smt2_incremental/smt_to_smt2_string.cpp 95.65% <0.00%> (ø)
...lvers/smt2_incremental/smt_response_validation.cpp 95.36% <0.00%> (ø)
... and 71 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

jimgrundy
jimgrundy approved these changes Oct 11, 2022
View reviewed changes
@tautschnig tautschnig force-pushed the bugfixes/7064-pointer-primitive-check branch 3 times, most recently from 2b28d8d to dc2a3e9 Compare October 11, 2022 08:51
@jimgrundy
Copy link
Collaborator

jimgrundy commented Oct 16, 2022

Assigning @kroening as the only active owner (other than the author) for the code in question.

kroening
kroening reviewed Oct 17, 2022
View reviewed changes
kroening
kroening reviewed Oct 17, 2022
View reviewed changes
@tautschnig
Pointer-primitive checks should succeed for valid pointers at object …
1c03453 
…bound

The C standard designates the pointer with offset object size (pointing
to the first byte outside the object) to be valid. In keeping with this,
`--pointer-primitive-check` should not designate this as invalid (even
when reading non-zero bytes from this object is).

Fixes: diffblue#7064
@tautschnig tautschnig force-pushed the bugfixes/7064-pointer-primitive-check branch from dc2a3e9 to 1c03453 Compare October 17, 2022 11:05
@tautschnig tautschnig merged commit d4f325b into diffblue:develop Oct 17, 2022
@tautschnig tautschnig deleted the bugfixes/7064-pointer-primitive-check branch October 17, 2022 12:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kroening kroening kroening approved these changes

@jimgrundy jimgrundy jimgrundy approved these changes

@chris-ryder chris-ryder Awaiting requested review from chris-ryder

@nwetzler nwetzler Awaiting requested review from nwetzler

Assignees

@tautschnig tautschnig

Labels

C Front End

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

--pointer-primitive-check fails on __CPROVER_r_ok(ptr, 0) when ptr = malloc(0)

5 participants

@tautschnig @jimgrundy @kroening @remi-delmas-3000 @nwetzler