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

Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked #3332

Merged
merged 8 commits into from
Jul 9, 2024
Merged

Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked #3332

Changes from 1 commit
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
5e97cd3
Make Kani reject casts between mutable pointers of different padding
artemagvanian Jul 8, 2024
08d4edc
Merge branch 'main' into reject-mut-ptr-casts
artemagvanian Jul 8, 2024
098d878
Format code
artemagvanian Jul 8, 2024
9d6d9e7
Make clippy happy
artemagvanian Jul 8, 2024
4092e82
Try format again
artemagvanian Jul 8, 2024
6dabe3f
Add copyright to the new test
artemagvanian Jul 8, 2024
4f97bab
Merge branch 'main' into reject-mut-ptr-casts
artemagvanian Jul 8, 2024
12b9a31
Merge branch 'main' into reject-mut-ptr-casts
artemagvanian Jul 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Make clippy happy
  • Loading branch information
@artemagvanian
artemagvanian committed Jul 8, 2024
commit 9d6d9e75cb7b97128a385ee6ee362c178cc766c9
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -739,8 +739,8 @@ fn try_resolve_instance(locals: &[LocalDecl], func: &Operand) -> Result<Instance
/// its size.
fn tys_layout_compatible(from_ty: &Ty, to_ty: &Ty) -> bool {
// Retrieve layouts to assess compatibility.
let from_ty_info = PointeeInfo::from_ty(from_ty.clone());
let to_ty_info = PointeeInfo::from_ty(to_ty.clone());
let from_ty_info = PointeeInfo::from_ty(*from_ty);
let to_ty_info = PointeeInfo::from_ty(*to_ty);
if let (Ok(from_ty_info), Ok(to_ty_info)) = (from_ty_info, to_ty_info) {
let from_ty_layout = match from_ty_info.layout() {
PointeeLayout::Sized { layout } => layout,
Expand Down
Loading