Skip to content

Spurious pointer overflow check failure #5284

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

Closed
danpoe opened this issue Mar 31, 2020 · 0 comments · Fixed by #5814
Closed

Spurious pointer overflow check failure #5284

danpoe opened this issue Mar 31, 2020 · 0 comments · Fixed by #5814

Comments

@danpoe
Copy link
Contributor

danpoe commented Mar 31, 2020

#include <stdlib.h>

void main()
{
  char *p = (char *)10;
  p -= 1;
  p += 1;
  p += -1; // spurious pointer overflow report
  p -= -1; // spurious pointer overflow report
}

CBMC version: 7e27cb2
Operating system: Ubuntu 16.04
Exact command line resulting in the issue: cbmc --pointer-overflow-check test.c
What behaviour did you expect: verification successful
What happened instead: spurious pointer overflow check failures

Regression test PR: #5283

tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 10, 2021
At a bare minimum, we should report an overflow when performing pointer
arithmetic that would result in an overflow on the underlying integer
representation.

As future work, we may want to expand on those checks by reporting
overflows when exceeding object bounds, as discussed in diffblue#5426.

Fixes: diffblue#5284
tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 11, 2021
At a bare minimum, we should report an overflow when performing pointer
arithmetic that would result in an overflow on the underlying integer
representation.

As future work, we may want to expand on those checks by reporting
overflows when exceeding object bounds, as discussed in diffblue#5426.

Fixes: diffblue#5284
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants