Basic tests for size_of_val and min_alig_of_val
#1101
Conversation
| enum MyEnum { | ||
| Variant, | ||
| } | ||
|
|
There was a problem hiding this comment.
Might be interesting to add a repr(C) struct which would require padding and make sure we get this right
There was a problem hiding this comment.
Added a repr(C) struct and assertions based on it. As far as I can tell, it's working as expected:
- Size takes into account padding
- Alignment is the max alignment for each field
But let me know if you want to test specific cases and I will add them.
| // SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
|
||
| // Check that we get the expected results for the `min_align_of_val` intrinsic | ||
| // with common data types |
There was a problem hiding this comment.
Is this architecture specific, of do these min aligns come from the rust spec?
There was a problem hiding this comment.
My understanding is that min_align_of_val depends on min_global_align, which is an architecture option.
Please note that in #1054 we added checks to ensure that min_global_align is unspecified or equal to 1, otherwise Kani will stop there.
There was a problem hiding this comment.
Can you add a comment that the tests here assume x86, otherwise good to go.
| // SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
|
||
| // Check that we get the expected results for the `min_align_of_val` intrinsic | ||
| // with common data types |
There was a problem hiding this comment.
Can you add a comment that the tests here assume x86, otherwise good to go.
* Basic tests for `size_of_val` and `min_alig_of_val` * Fix format * Add cases for `repr(C)` struct * Add note
Description of changes:
Adds two tests for
size_of_valandmin_align_of_val.@celinval added tests for dynamically-sized types in #1089 , these ones just complement them by testing basic types.
Resolved issues:
Part of #727
Call-outs:
Testing:
How is this change tested? Adds two tests.
Is this a refactor change? No.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.