@@ -537,7 +537,7 @@ impl Queue {
537
537
return self . pop ( mem) ;
538
538
}
539
539
540
- if self . try_enable_notification ( mem ) {
540
+ if self . try_enable_notification ( ) {
541
541
return None ;
542
542
}
543
543
@@ -614,9 +614,7 @@ impl Queue {
614
614
/// successfully enabled. Otherwise it means that one or more descriptors can still be consumed
615
615
/// from the available ring and we can't guarantee that there will be a notification. In this
616
616
/// case the caller might want to consume the mentioned descriptors and call this method again.
617
- pub fn try_enable_notification < M : GuestMemory > ( & mut self , mem : & M ) -> bool {
618
- debug_assert ! ( self . is_valid( mem) ) ;
619
-
617
+ pub fn try_enable_notification ( & mut self ) -> bool {
620
618
// If the device doesn't use notification suppression, we'll continue to get notifications
621
619
// no matter what.
622
620
if !self . uses_notif_suppression {
@@ -1129,11 +1127,11 @@ mod verification {
1129
1127
#[ kani:: proof]
1130
1128
#[ kani:: unwind( 0 ) ]
1131
1129
fn verify_try_enable_notification ( ) {
1132
- let ProofContext ( mut queue, mem ) = ProofContext :: bounded_queue ( ) ;
1130
+ let ProofContext ( mut queue, _ ) = ProofContext :: bounded_queue ( ) ;
1133
1131
1134
1132
kani:: assume ( queue. len ( ) <= queue. actual_size ( ) ) ;
1135
1133
1136
- if queue. try_enable_notification ( & mem ) && queue. uses_notif_suppression {
1134
+ if queue. try_enable_notification ( ) && queue. uses_notif_suppression {
1137
1135
// We only require new notifications if the queue is empty (e.g. we've processed
1138
1136
// everything we've been notified about), or if suppression is disabled.
1139
1137
assert ! ( queue. is_empty( ) ) ;
@@ -1584,18 +1582,18 @@ mod tests {
1584
1582
assert_eq ! ( q. len( ) , 1 ) ;
1585
1583
1586
1584
// Notification suppression is disabled. try_enable_notification shouldn't do anything.
1587
- assert ! ( q. try_enable_notification( m ) ) ;
1585
+ assert ! ( q. try_enable_notification( ) ) ;
1588
1586
assert_eq ! ( q. avail_event( m) , 0 ) ;
1589
1587
1590
1588
// Enable notification suppression and check again. There is 1 available descriptor chain.
1591
1589
// Again nothing should happen.
1592
1590
q. enable_notif_suppression ( ) ;
1593
- assert ! ( !q. try_enable_notification( m ) ) ;
1591
+ assert ! ( !q. try_enable_notification( ) ) ;
1594
1592
assert_eq ! ( q. avail_event( m) , 0 ) ;
1595
1593
1596
1594
// Consume the descriptor. avail_event should be modified
1597
1595
assert ! ( q. pop( m) . is_some( ) ) ;
1598
- assert ! ( q. try_enable_notification( m ) ) ;
1596
+ assert ! ( q. try_enable_notification( ) ) ;
1599
1597
assert_eq ! ( q. avail_event( m) , 1 ) ;
1600
1598
}
1601
1599
0 commit comments