Skip to content

Commit fb8ad3e

Browse files
tautschnigtautschnig
committed
rustfmt
1 parent 0a7a3c6 commit fb8ad3e

File tree

1 file changed

+301
-49
lines changed

1 file changed

+301
-49
lines changed

‎library/core/src/num/nonzero.rs‎

Lines changed: 301 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -2418,17 +2418,57 @@ mod verify {
24182418

24192419
// Use the macro to generate different versions of the function for multiple types
24202420
nonzero_check!(i8, core::num::NonZeroI8, nonzero_check_new_unchecked_for_i8);
2421-
nonzero_check!(i16, core::num::NonZeroI16, nonzero_check_new_unchecked_for_16);
2422-
nonzero_check!(i32, core::num::NonZeroI32, nonzero_check_new_unchecked_for_32);
2423-
nonzero_check!(i64, core::num::NonZeroI64, nonzero_check_new_unchecked_for_64);
2424-
nonzero_check!(i128, core::num::NonZeroI128, nonzero_check_new_unchecked_for_128);
2425-
nonzero_check!(isize, core::num::NonZeroIsize, nonzero_check_new_unchecked_for_isize);
2421+
nonzero_check!(
2422+
i16,
2423+
core::num::NonZeroI16,
2424+
nonzero_check_new_unchecked_for_16
2425+
);
2426+
nonzero_check!(
2427+
i32,
2428+
core::num::NonZeroI32,
2429+
nonzero_check_new_unchecked_for_32
2430+
);
2431+
nonzero_check!(
2432+
i64,
2433+
core::num::NonZeroI64,
2434+
nonzero_check_new_unchecked_for_64
2435+
);
2436+
nonzero_check!(
2437+
i128,
2438+
core::num::NonZeroI128,
2439+
nonzero_check_new_unchecked_for_128
2440+
);
2441+
nonzero_check!(
2442+
isize,
2443+
core::num::NonZeroIsize,
2444+
nonzero_check_new_unchecked_for_isize
2445+
);
24262446
nonzero_check!(u8, core::num::NonZeroU8, nonzero_check_new_unchecked_for_u8);
2427-
nonzero_check!(u16, core::num::NonZeroU16, nonzero_check_new_unchecked_for_u16);
2428-
nonzero_check!(u32, core::num::NonZeroU32, nonzero_check_new_unchecked_for_u32);
2429-
nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64);
2430-
nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128);
2431-
nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize);
2447+
nonzero_check!(
2448+
u16,
2449+
core::num::NonZeroU16,
2450+
nonzero_check_new_unchecked_for_u16
2451+
);
2452+
nonzero_check!(
2453+
u32,
2454+
core::num::NonZeroU32,
2455+
nonzero_check_new_unchecked_for_u32
2456+
);
2457+
nonzero_check!(
2458+
u64,
2459+
core::num::NonZeroU64,
2460+
nonzero_check_new_unchecked_for_u64
2461+
);
2462+
nonzero_check!(
2463+
u128,
2464+
core::num::NonZeroU128,
2465+
nonzero_check_new_unchecked_for_u128
2466+
);
2467+
nonzero_check!(
2468+
usize,
2469+
core::num::NonZeroUsize,
2470+
nonzero_check_new_unchecked_for_usize
2471+
);
24322472

24332473
// macro_rules! nonzero_check_from_mut_unchecked {
24342474
// ($t:ty, $nonzero_type:ty, $harness_name:ident) => {
@@ -2670,7 +2710,7 @@ mod verify {
26702710
nonzero_check_rotate_left_and_right!(core::num::NonZeroU128, nonzero_check_rotate_for_u128);
26712711
nonzero_check_rotate_left_and_right!(core::num::NonZeroUsize, nonzero_check_rotate_for_usize);
26722712

2673-
macro_rules! check_mul_unchecked_small{
2713+
macro_rules! check_mul_unchecked_small {
26742714
($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_mul_for:ident) => {
26752715
#[kani::proof_for_contract(<$t>::unchecked_mul)]
26762716
pub fn $nonzero_check_unchecked_mul_for() {
@@ -2684,7 +2724,7 @@ mod verify {
26842724
};
26852725
}
26862726

2687-
macro_rules! check_mul_unchecked_intervals{
2727+
macro_rules! check_mul_unchecked_intervals {
26882728
($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => {
26892729
#[kani::proof_for_contract(<$t>::unchecked_mul)]
26902730
pub fn $nonzero_check_mul_for() {
@@ -2705,52 +2745,244 @@ mod verify {
27052745
}
27062746

27072747
//Calls for i32
2708-
check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_small, NonZeroI32::new(-10i32).unwrap().into(), NonZeroI32::new(10i32).unwrap().into());
2709-
check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_pos, NonZeroI32::new(i32::MAX - 1000i32).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into());
2710-
check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_neg, NonZeroI32::new(i32::MIN + 1000i32).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into());
2711-
check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_pos, NonZeroI32::new(i32::MAX / 2).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into());
2712-
check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_neg, NonZeroI32::new(i32::MIN / 2).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into());
2748+
check_mul_unchecked_intervals!(
2749+
i32,
2750+
NonZeroI32,
2751+
check_mul_i32_small,
2752+
NonZeroI32::new(-10i32).unwrap().into(),
2753+
NonZeroI32::new(10i32).unwrap().into()
2754+
);
2755+
check_mul_unchecked_intervals!(
2756+
i32,
2757+
NonZeroI32,
2758+
check_mul_i32_large_pos,
2759+
NonZeroI32::new(i32::MAX - 1000i32).unwrap().into(),
2760+
NonZeroI32::new(i32::MAX).unwrap().into()
2761+
);
2762+
check_mul_unchecked_intervals!(
2763+
i32,
2764+
NonZeroI32,
2765+
check_mul_i32_large_neg,
2766+
NonZeroI32::new(i32::MIN + 1000i32).unwrap().into(),
2767+
NonZeroI32::new(i32::MIN + 1).unwrap().into()
2768+
);
2769+
check_mul_unchecked_intervals!(
2770+
i32,
2771+
NonZeroI32,
2772+
check_mul_i32_edge_pos,
2773+
NonZeroI32::new(i32::MAX / 2).unwrap().into(),
2774+
NonZeroI32::new(i32::MAX).unwrap().into()
2775+
);
2776+
check_mul_unchecked_intervals!(
2777+
i32,
2778+
NonZeroI32,
2779+
check_mul_i32_edge_neg,
2780+
NonZeroI32::new(i32::MIN / 2).unwrap().into(),
2781+
NonZeroI32::new(i32::MIN + 1).unwrap().into()
2782+
);
27132783

27142784
//Calls for i64
2715-
check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_small, NonZeroI64::new(-10i64).unwrap().into(), NonZeroI64::new(10i64).unwrap().into());
2716-
check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_pos, NonZeroI64::new(i64::MAX - 1000i64).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into());
2717-
check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_neg, NonZeroI64::new(i64::MIN + 1000i64).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into());
2718-
check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_pos, NonZeroI64::new(i64::MAX / 2).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into());
2719-
check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_neg, NonZeroI64::new(i64::MIN / 2).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into());
2785+
check_mul_unchecked_intervals!(
2786+
i64,
2787+
NonZeroI64,
2788+
check_mul_i64_small,
2789+
NonZeroI64::new(-10i64).unwrap().into(),
2790+
NonZeroI64::new(10i64).unwrap().into()
2791+
);
2792+
check_mul_unchecked_intervals!(
2793+
i64,
2794+
NonZeroI64,
2795+
check_mul_i64_large_pos,
2796+
NonZeroI64::new(i64::MAX - 1000i64).unwrap().into(),
2797+
NonZeroI64::new(i64::MAX).unwrap().into()
2798+
);
2799+
check_mul_unchecked_intervals!(
2800+
i64,
2801+
NonZeroI64,
2802+
check_mul_i64_large_neg,
2803+
NonZeroI64::new(i64::MIN + 1000i64).unwrap().into(),
2804+
NonZeroI64::new(i64::MIN + 1).unwrap().into()
2805+
);
2806+
check_mul_unchecked_intervals!(
2807+
i64,
2808+
NonZeroI64,
2809+
check_mul_i64_edge_pos,
2810+
NonZeroI64::new(i64::MAX / 2).unwrap().into(),
2811+
NonZeroI64::new(i64::MAX).unwrap().into()
2812+
);
2813+
check_mul_unchecked_intervals!(
2814+
i64,
2815+
NonZeroI64,
2816+
check_mul_i64_edge_neg,
2817+
NonZeroI64::new(i64::MIN / 2).unwrap().into(),
2818+
NonZeroI64::new(i64::MIN + 1).unwrap().into()
2819+
);
27202820

27212821
//calls for i128
2722-
check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_small, NonZeroI128::new(-10i128).unwrap().into(), NonZeroI128::new(10i128).unwrap().into());
2723-
check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_pos, NonZeroI128::new(i128::MAX - 1000i128).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into());
2724-
check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_neg, NonZeroI128::new(i128::MIN + 1000i128).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into());
2725-
check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_pos, NonZeroI128::new(i128::MAX / 2).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into());
2726-
check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_neg, NonZeroI128::new(i128::MIN / 2).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into());
2822+
check_mul_unchecked_intervals!(
2823+
i128,
2824+
NonZeroI128,
2825+
check_mul_i128_small,
2826+
NonZeroI128::new(-10i128).unwrap().into(),
2827+
NonZeroI128::new(10i128).unwrap().into()
2828+
);
2829+
check_mul_unchecked_intervals!(
2830+
i128,
2831+
NonZeroI128,
2832+
check_mul_i128_large_pos,
2833+
NonZeroI128::new(i128::MAX - 1000i128).unwrap().into(),
2834+
NonZeroI128::new(i128::MAX).unwrap().into()
2835+
);
2836+
check_mul_unchecked_intervals!(
2837+
i128,
2838+
NonZeroI128,
2839+
check_mul_i128_large_neg,
2840+
NonZeroI128::new(i128::MIN + 1000i128).unwrap().into(),
2841+
NonZeroI128::new(i128::MIN + 1).unwrap().into()
2842+
);
2843+
check_mul_unchecked_intervals!(
2844+
i128,
2845+
NonZeroI128,
2846+
check_mul_i128_edge_pos,
2847+
NonZeroI128::new(i128::MAX / 2).unwrap().into(),
2848+
NonZeroI128::new(i128::MAX).unwrap().into()
2849+
);
2850+
check_mul_unchecked_intervals!(
2851+
i128,
2852+
NonZeroI128,
2853+
check_mul_i128_edge_neg,
2854+
NonZeroI128::new(i128::MIN / 2).unwrap().into(),
2855+
NonZeroI128::new(i128::MIN + 1).unwrap().into()
2856+
);
27272857

27282858
//calls for isize
2729-
check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_small, NonZeroIsize::new(-10isize).unwrap().into(), NonZeroIsize::new(10isize).unwrap().into());
2730-
check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_pos, NonZeroIsize::new(isize::MAX - 1000isize).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into());
2731-
check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_neg, NonZeroIsize::new(isize::MIN + 1000isize).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into());
2732-
check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_pos, NonZeroIsize::new(isize::MAX / 2).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into());
2733-
check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_neg, NonZeroIsize::new(isize::MIN / 2).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into());
2859+
check_mul_unchecked_intervals!(
2860+
isize,
2861+
NonZeroIsize,
2862+
check_mul_isize_small,
2863+
NonZeroIsize::new(-10isize).unwrap().into(),
2864+
NonZeroIsize::new(10isize).unwrap().into()
2865+
);
2866+
check_mul_unchecked_intervals!(
2867+
isize,
2868+
NonZeroIsize,
2869+
check_mul_isize_large_pos,
2870+
NonZeroIsize::new(isize::MAX - 1000isize).unwrap().into(),
2871+
NonZeroIsize::new(isize::MAX).unwrap().into()
2872+
);
2873+
check_mul_unchecked_intervals!(
2874+
isize,
2875+
NonZeroIsize,
2876+
check_mul_isize_large_neg,
2877+
NonZeroIsize::new(isize::MIN + 1000isize).unwrap().into(),
2878+
NonZeroIsize::new(isize::MIN + 1).unwrap().into()
2879+
);
2880+
check_mul_unchecked_intervals!(
2881+
isize,
2882+
NonZeroIsize,
2883+
check_mul_isize_edge_pos,
2884+
NonZeroIsize::new(isize::MAX / 2).unwrap().into(),
2885+
NonZeroIsize::new(isize::MAX).unwrap().into()
2886+
);
2887+
check_mul_unchecked_intervals!(
2888+
isize,
2889+
NonZeroIsize,
2890+
check_mul_isize_edge_neg,
2891+
NonZeroIsize::new(isize::MIN / 2).unwrap().into(),
2892+
NonZeroIsize::new(isize::MIN + 1).unwrap().into()
2893+
);
27342894

27352895
//calls for u32
2736-
check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_small, NonZeroU32::new(1u32).unwrap().into(), NonZeroU32::new(10u32).unwrap().into());
2737-
check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_large, NonZeroU32::new(u32::MAX - 1000u32).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into());
2738-
check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_edge, NonZeroU32::new(u32::MAX / 2).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into());
2896+
check_mul_unchecked_intervals!(
2897+
u32,
2898+
NonZeroU32,
2899+
check_mul_u32_small,
2900+
NonZeroU32::new(1u32).unwrap().into(),
2901+
NonZeroU32::new(10u32).unwrap().into()
2902+
);
2903+
check_mul_unchecked_intervals!(
2904+
u32,
2905+
NonZeroU32,
2906+
check_mul_u32_large,
2907+
NonZeroU32::new(u32::MAX - 1000u32).unwrap().into(),
2908+
NonZeroU32::new(u32::MAX).unwrap().into()
2909+
);
2910+
check_mul_unchecked_intervals!(
2911+
u32,
2912+
NonZeroU32,
2913+
check_mul_u32_edge,
2914+
NonZeroU32::new(u32::MAX / 2).unwrap().into(),
2915+
NonZeroU32::new(u32::MAX).unwrap().into()
2916+
);
27392917

27402918
//calls for u64
2741-
check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_small, NonZeroU64::new(1u64).unwrap().into(), NonZeroU64::new(10u64).unwrap().into());
2742-
check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_large, NonZeroU64::new(u64::MAX - 1000u64).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into());
2743-
check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_edge, NonZeroU64::new(u64::MAX / 2).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into());
2919+
check_mul_unchecked_intervals!(
2920+
u64,
2921+
NonZeroU64,
2922+
check_mul_u64_small,
2923+
NonZeroU64::new(1u64).unwrap().into(),
2924+
NonZeroU64::new(10u64).unwrap().into()
2925+
);
2926+
check_mul_unchecked_intervals!(
2927+
u64,
2928+
NonZeroU64,
2929+
check_mul_u64_large,
2930+
NonZeroU64::new(u64::MAX - 1000u64).unwrap().into(),
2931+
NonZeroU64::new(u64::MAX).unwrap().into()
2932+
);
2933+
check_mul_unchecked_intervals!(
2934+
u64,
2935+
NonZeroU64,
2936+
check_mul_u64_edge,
2937+
NonZeroU64::new(u64::MAX / 2).unwrap().into(),
2938+
NonZeroU64::new(u64::MAX).unwrap().into()
2939+
);
27442940

27452941
//calls for u128
2746-
check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_small, NonZeroU128::new(1u128).unwrap().into(), NonZeroU128::new(10u128).unwrap().into());
2747-
check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_large, NonZeroU128::new(u128::MAX - 1000u128).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into());
2748-
check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_edge, NonZeroU128::new(u128::MAX / 2).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into());
2942+
check_mul_unchecked_intervals!(
2943+
u128,
2944+
NonZeroU128,
2945+
check_mul_u128_small,
2946+
NonZeroU128::new(1u128).unwrap().into(),
2947+
NonZeroU128::new(10u128).unwrap().into()
2948+
);
2949+
check_mul_unchecked_intervals!(
2950+
u128,
2951+
NonZeroU128,
2952+
check_mul_u128_large,
2953+
NonZeroU128::new(u128::MAX - 1000u128).unwrap().into(),
2954+
NonZeroU128::new(u128::MAX).unwrap().into()
2955+
);
2956+
check_mul_unchecked_intervals!(
2957+
u128,
2958+
NonZeroU128,
2959+
check_mul_u128_edge,
2960+
NonZeroU128::new(u128::MAX / 2).unwrap().into(),
2961+
NonZeroU128::new(u128::MAX).unwrap().into()
2962+
);
27492963

27502964
//calls for usize
2751-
check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_small, NonZeroUsize::new(1usize).unwrap().into(), NonZeroUsize::new(10usize).unwrap().into());
2752-
check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_large, NonZeroUsize::new(usize::MAX - 1000usize).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into());
2753-
check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_edge, NonZeroUsize::new(usize::MAX / 2).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into());
2965+
check_mul_unchecked_intervals!(
2966+
usize,
2967+
NonZeroUsize,
2968+
check_mul_usize_small,
2969+
NonZeroUsize::new(1usize).unwrap().into(),
2970+
NonZeroUsize::new(10usize).unwrap().into()
2971+
);
2972+
check_mul_unchecked_intervals!(
2973+
usize,
2974+
NonZeroUsize,
2975+
check_mul_usize_large,
2976+
NonZeroUsize::new(usize::MAX - 1000usize).unwrap().into(),
2977+
NonZeroUsize::new(usize::MAX).unwrap().into()
2978+
);
2979+
check_mul_unchecked_intervals!(
2980+
usize,
2981+
NonZeroUsize,
2982+
check_mul_usize_edge,
2983+
NonZeroUsize::new(usize::MAX / 2).unwrap().into(),
2984+
NonZeroUsize::new(usize::MAX).unwrap().into()
2985+
);
27542986

27552987
//calls for i8, i16, u8, u16
27562988
check_mul_unchecked_small!(i8, NonZeroI8, nonzero_check_mul_for_i8);
@@ -2782,9 +3014,29 @@ mod verify {
27823014
// nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128);
27833015
// nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize);
27843016
nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8);
2785-
nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16);
2786-
nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32);
2787-
nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64);
2788-
nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128);
2789-
nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize);
3017+
nonzero_check_add!(
3018+
u16,
3019+
core::num::NonZeroU16,
3020+
nonzero_check_unchecked_add_for_u16
3021+
);
3022+
nonzero_check_add!(
3023+
u32,
3024+
core::num::NonZeroU32,
3025+
nonzero_check_unchecked_add_for_u32
3026+
);
3027+
nonzero_check_add!(
3028+
u64,
3029+
core::num::NonZeroU64,
3030+
nonzero_check_unchecked_add_for_u64
3031+
);
3032+
nonzero_check_add!(
3033+
u128,
3034+
core::num::NonZeroU128,
3035+
nonzero_check_unchecked_add_for_u128
3036+
);
3037+
nonzero_check_add!(
3038+
usize,
3039+
core::num::NonZeroUsize,
3040+
nonzero_check_unchecked_add_for_usize
3041+
);
27903042
}

0 commit comments

Comments
 (0)