@@ -2592,7 +2592,7 @@ mod verify {
2592
2592
2593
2593
macro_rules! check_mul_unchecked_small {
2594
2594
( $t: ty, $nonzero_type: ty, $nonzero_check_unchecked_mul_for: ident) => {
2595
- #[ kani:: proof_for_contract( <$t>:: unchecked_mul) ]
2595
+ #[ kani:: proof_for_contract( NonZero :: <$t>:: unchecked_mul) ]
2596
2596
pub fn $nonzero_check_unchecked_mul_for( ) {
2597
2597
let x: $nonzero_type = kani:: any( ) ;
2598
2598
let y: $nonzero_type = kani:: any( ) ;
@@ -2606,7 +2606,7 @@ mod verify {
2606
2606
2607
2607
macro_rules! check_mul_unchecked_intervals {
2608
2608
( $t: ty, $nonzero_type: ty, $nonzero_check_mul_for: ident, $min: expr, $max: expr) => {
2609
- #[ kani:: proof_for_contract( <$t>:: unchecked_mul) ]
2609
+ #[ kani:: proof_for_contract( NonZero :: <$t>:: unchecked_mul) ]
2610
2610
pub fn $nonzero_check_mul_for( ) {
2611
2611
let x = kani:: any:: <$t>( ) ;
2612
2612
let y = kani:: any:: <$t>( ) ;
@@ -2872,7 +2872,7 @@ mod verify {
2872
2872
2873
2873
macro_rules! nonzero_check_add {
2874
2874
( $t: ty, $nonzero_type: ty, $nonzero_check_unchecked_add_for: ident) => {
2875
- #[ kani:: proof_for_contract( <$t>:: unchecked_add) ]
2875
+ #[ kani:: proof_for_contract( NonZero :: <$t>:: unchecked_add) ]
2876
2876
pub fn $nonzero_check_unchecked_add_for( ) {
2877
2877
let x: $nonzero_type = kani:: any( ) ;
2878
2878
let y: $t = kani:: any( ) ;
0 commit comments