@@ -614,8 +614,8 @@ mod verify {
614
614
#[ kani:: proof]
615
615
pub fn $harness_pass( ) {
616
616
let x_inner: $source = kani:: any_where( |& v| {
617
- ( v > 0 && ( v as u128 ) <= ( <$target>:: MAX as u128 ) ) ||
618
- ( v < 0 && ( v as i128 ) >= ( <$target>:: MIN as i128 ) )
617
+ ( v > 0 && ( v as u128 ) <= ( <$target>:: MAX as u128 ) )
618
+ || ( v < 0 && ( v as i128 ) >= ( <$target>:: MIN as i128 ) )
619
619
} ) ;
620
620
let x = NonZero :: new( x_inner) . unwrap( ) ;
621
621
let _ = NonZero :: <$target>:: try_from( x) . unwrap( ) ;
@@ -625,8 +625,8 @@ mod verify {
625
625
#[ kani:: should_panic]
626
626
pub fn $harness_panic( ) {
627
627
let x_inner: $source = kani:: any_where( |& v| {
628
- ( v > 0 && ( v as u128 ) > ( <$target>:: MAX as u128 ) ) ||
629
- ( v < 0 && ( v as i128 ) < ( <$target>:: MIN as i128 ) )
628
+ ( v > 0 && ( v as u128 ) > ( <$target>:: MAX as u128 ) )
629
+ || ( v < 0 && ( v as i128 ) < ( <$target>:: MIN as i128 ) )
630
630
} ) ;
631
631
let x = NonZero :: new( x_inner) . unwrap( ) ;
632
632
let _ = NonZero :: <$target>:: try_from( x) . unwrap( ) ;
@@ -635,10 +635,10 @@ mod verify {
635
635
( $source: ty => $target: ty, $harness_infallible: ident, ) => {
636
636
#[ kani:: proof]
637
637
pub fn $harness_infallible( ) {
638
- let x: NonZero :: <$source> = kani:: any( ) ;
638
+ let x: NonZero <$source> = kani:: any( ) ;
639
639
let _ = NonZero :: <$target>:: try_from( x) . unwrap( ) ;
640
640
}
641
- }
641
+ } ;
642
642
}
643
643
644
644
// unsigned non-zero integer -> unsigned non-zero integer fallible
0 commit comments