Skip to content

Crash on pointer dereference for pointer constrained with assumption #5328

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.

Sign up for GitHub

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

Jump to bottom
Closed
danpoe opened this issue Apr 30, 2020 · 1 comment · Fixed by #6044
Closed

Crash on pointer dereference for pointer constrained with assumption #5328

danpoe opened this issue Apr 30, 2020 · 1 comment · Fixed by #6044
Labels
pending merge

Comments

@danpoe
Copy link
Contributor

danpoe commented Apr 30, 2020 

#include <assert.h>
#include <stdlib.h>

void main()
{
  char *p;
  __CPROVER_assume(__CPROVER_r_ok(p - 1, 1));
  *p;
}

CBMC version: 03ab5c7
Operating system: Ubuntu
Exact command line resulting in the issue: cbmc --pointer-check --no-simplify --no-propagation main.c
What behaviour did you expect: verification failed
What happened instead: crash
@danpoe danpoe mentioned this issue May 1, 2020
Merged
3 tasks
@danielsn
Copy link
Contributor

danielsn commented May 4, 2020

May be related to #5293

tautschnig added a commit to tautschnig/cbmc that referenced this issue Apr 16, 2021
@tautschnig
Pointer subtraction was fixed in 3acdb52
d19fb6a 
The invariant failure was caused by a bug in handling pointer
subtraction, which was fixed in 3acdb52. The test also wrongly assumed
verification would succeed, which is not correct for `*p`, which is out
of bounds.

Fixes: diffblue#5328
@tautschnig tautschnig mentioned this issue Apr 16, 2021
Merged
3 tasks
tautschnig added a commit to tautschnig/cbmc that referenced this issue Apr 16, 2021
@tautschnig
Pointer subtraction was fixed in 3acdb52
e94daaa 
The invariant failure was caused by a bug in handling pointer
subtraction, which was fixed in 3acdb52. The test also wrongly assumed
verification would succeed, which is not correct for `*p`, which is out
of bounds.

Fixes: diffblue#5328
jezhiggins pushed a commit to jezhiggins/cbmc that referenced this issue Apr 23, 2021
@tautschnig @jezhiggins
Pointer subtraction was fixed in 3acdb52
517b9d0 
The invariant failure was caused by a bug in handling pointer
subtraction, which was fixed in 3acdb52. The test also wrongly assumed
verification would succeed, which is not correct for `*p`, which is out
of bounds.

Fixes: diffblue#5328
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Pointer subtraction was fixed in 3acdb52dd tautschnig/cbmc
3 participants
@tautschnig @danielsn @danpoe