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.

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

Kani implementations of mem::size_of_val and mem::align_of_val are incorrect for traits #1074

Closed
celinval opened this issue Apr 20, 2022 · 1 comment · Fixed by #1089
Closed

Kani implementations of mem::size_of_val and mem::align_of_val are incorrect for traits #1074

celinval opened this issue Apr 20, 2022 · 1 comment · Fixed by #1089
Assignees
@celinval
Labels
[C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue

Comments

@celinval
Copy link
Contributor

I added a test case here: tests/kani/Intrinsics/SizeOfVal/fixme_size_of_fat_ptr.rs

It fails due to incorrect implementation of size_of_val. See test for more details.
@celinval celinval added the [C] Bug This is a bug. Something isn't working. label Apr 20, 2022
@celinval celinval added Soundness: Medium [F] Soundness Kani failed to detect an issue and removed Soundness: Medium labels Apr 20, 2022
@celinval celinval assigned celinval and unassigned adpaco-aws Apr 20, 2022
@celinval
Copy link
Contributor Author

We cannot handle type of traits. Until we support that, we should fail the verification for dyn T.

@celinval celinval changed the title Kani implementation of mem::size_of_val is incorrect for unsized struct Kani implementations of mem::size_of_val and mem::align_of_val are incorrect for unsized struct Apr 21, 2022
@celinval celinval changed the title Kani implementations of mem::size_of_val and mem::align_of_val are incorrect for unsized struct Kani implementations of mem::size_of_val and mem::align_of_val are incorrect for traits Apr 21, 2022
@celinval celinval mentioned this issue Apr 21, 2022
Merged
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@celinval celinval

Labels
[C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix issue with value_of / align_of traits celinval/kani-dev
3 participants
@celinval @nchong-at-aws @adpaco-aws