Skip to content
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

Avoid usage of __CPROVER_havoc_object #653

Open
adpaco-aws opened this issue Dec 3, 2020 · 0 comments
Open

Avoid usage of __CPROVER_havoc_object #653

adpaco-aws opened this issue Dec 3, 2020 · 0 comments
Labels
cbmc CBMC proof related work

Comments

@adpaco-aws
Copy link
Collaborator

A call to __CPROVER_havoc_object will overwrite an entire CBMC object. If the pointer being passed to write_unconstrained_data is part of a larger struct, CBMC will overwrite the larger struct:

void write_unconstrained_data(unsigned char *out, size_t len) {
assert(AWS_MEM_IS_WRITABLE(out, len));
// Currently we ignore the len parameter and just fill the entire buffer with unconstrained data.
// This is fine because it is strictly more general behavior than writing only len bytes.
__CPROVER_havoc_object(out);
}

Issues related: #652

@adpaco-aws adpaco-aws added the cbmc CBMC proof related work label Dec 3, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
cbmc CBMC proof related work
Projects
None yet
Development

No branches or pull requests

1 participant