Skip to content

Commit

Permalink
Merge pull request #2 from stogaru/verify/ptr_const_composite
Browse files Browse the repository at this point in the history
Adds proofs for composite type - tuple
  • Loading branch information
stogaru authored Oct 3, 2024
2 parents 6853284 + 7d05c96 commit 8e49dcd
Showing 1 changed file with 14 additions and 2 deletions.
16 changes: 14 additions & 2 deletions library/core/src/ptr/const_ptr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1823,7 +1823,11 @@ mod verify {
generate_add_harness!(u32, check_add_u32);
generate_add_harness!(u64, check_add_u64);
generate_add_harness!(u128, check_add_u128);
generate_add_harness!(usize, check_add_usize);
generate_add_harness!(usize, check_add_usize);
generate_add_harness!((i8, i8), check_add_tuple_1);
generate_add_harness!((f64, bool), check_add_tuple_2);
generate_add_harness!((i32, f64, bool), check_add_tuple_3);
generate_add_harness!((i8, u16, i32, u64, isize), check_add_tuple_4);
// fn <*const T>::add verification end

// fn <*const T>::sub verification begin
Expand Down Expand Up @@ -1853,7 +1857,11 @@ mod verify {
generate_sub_harness!(u32, check_sub_u32);
generate_sub_harness!(u64, check_sub_u64);
generate_sub_harness!(u128, check_sub_u128);
generate_sub_harness!(usize, check_sub_usize);
generate_sub_harness!(usize, check_sub_usize);
generate_sub_harness!((i8, i8), check_sub_tuple_1);
generate_sub_harness!((f64, bool), check_sub_tuple_2);
generate_sub_harness!((i32, f64, bool), check_sub_tuple_3);
generate_sub_harness!((i8, u16, i32, u64, isize), check_sub_tuple_4);
// fn <*const T>::sub verification end

// fn <*const T>::offset verification begin
Expand Down Expand Up @@ -1884,6 +1892,10 @@ mod verify {
generate_offset_harness!(u64, check_offset_u64);
generate_offset_harness!(u128, check_offset_u128);
generate_offset_harness!(usize, check_offset_usize);
generate_offset_harness!((i8, i8), check_offset_tuple_1);
generate_offset_harness!((f64, bool), check_offset_tuple_2);
generate_offset_harness!((i32, f64, bool), check_offset_tuple_3);
generate_offset_harness!((i8, u16, i32, u64, isize), check_offset_tuple_4);
// fn <*const T>::offset verification end

}

0 comments on commit 8e49dcd

Please sign in to comment.