@@ -657,9 +657,7 @@ impl Queue {
657
657
/// updates `used_event` and/or the notification conditions hold once more.
658
658
///
659
659
/// This is similar to the `vring_need_event()` method implemented by the Linux kernel.
660
- pub fn prepare_kick < M : GuestMemory > ( & mut self , mem : & M ) -> bool {
661
- debug_assert ! ( self . is_valid( mem) ) ;
662
-
660
+ pub fn prepare_kick ( & mut self ) -> bool {
663
661
// If the device doesn't use notification suppression, always return true
664
662
if !self . uses_notif_suppression {
665
663
return true ;
@@ -954,10 +952,10 @@ mod verification {
954
952
// has been processed. This is done by the driver
955
953
// defining a "used_event" index, which tells the device "please do not notify me until
956
954
// used.ring[used_event] has been written to by you".
957
- let ProofContext ( mut queue, mem ) = ProofContext :: bounded_queue ( ) ;
955
+ let ProofContext ( mut queue, _ ) = ProofContext :: bounded_queue ( ) ;
958
956
959
957
let num_added_old = queue. num_added . 0 ;
960
- let needs_notification = queue. prepare_kick ( & mem ) ;
958
+ let needs_notification = queue. prepare_kick ( ) ;
961
959
962
960
// uses_notif_suppression equivalent to VIRTIO_F_EVENT_IDX negotiated
963
961
if !queue. uses_notif_suppression {
@@ -995,7 +993,7 @@ mod verification {
995
993
// number of added descriptors being counted in Queue.num_added), and then use
996
994
// "prepare_kick" to check if any of those descriptors should have triggered a
997
995
// notification.
998
- let ProofContext ( mut queue, mem ) = ProofContext :: bounded_queue ( ) ;
996
+ let ProofContext ( mut queue, _ ) = ProofContext :: bounded_queue ( ) ;
999
997
1000
998
queue. enable_notif_suppression ( ) ;
1001
999
assert ! ( queue. uses_notif_suppression) ;
@@ -1023,7 +1021,7 @@ mod verification {
1023
1021
used_event >= interval_start && used_event <= interval_end
1024
1022
} ;
1025
1023
1026
- assert_eq ! ( queue. prepare_kick( & mem ) , needs_notification) ;
1024
+ assert_eq ! ( queue. prepare_kick( ) , needs_notification) ;
1027
1025
}
1028
1026
1029
1027
#[ kani:: proof]
@@ -1529,7 +1527,7 @@ mod tests {
1529
1527
q. next_used = Wrapping ( used_idx) ;
1530
1528
vq. avail . event . set ( used_event) ;
1531
1529
q. num_added = Wrapping ( num_added) ;
1532
- assert ! ( q. prepare_kick( m ) ) ;
1530
+ assert ! ( q. prepare_kick( ) ) ;
1533
1531
}
1534
1532
}
1535
1533
}
@@ -1541,23 +1539,23 @@ mod tests {
1541
1539
q. next_used = Wrapping ( 10 ) ;
1542
1540
vq. avail . event . set ( 6 ) ;
1543
1541
q. num_added = Wrapping ( 5 ) ;
1544
- assert ! ( q. prepare_kick( m ) ) ;
1542
+ assert ! ( q. prepare_kick( ) ) ;
1545
1543
}
1546
1544
1547
1545
{
1548
1546
// old used idx = used_event < next_used
1549
1547
q. next_used = Wrapping ( 10 ) ;
1550
1548
vq. avail . event . set ( 6 ) ;
1551
1549
q. num_added = Wrapping ( 4 ) ;
1552
- assert ! ( q. prepare_kick( m ) ) ;
1550
+ assert ! ( q. prepare_kick( ) ) ;
1553
1551
}
1554
1552
1555
1553
{
1556
1554
// used_event < old used idx < next_used
1557
1555
q. next_used = Wrapping ( 10 ) ;
1558
1556
vq. avail . event . set ( 6 ) ;
1559
1557
q. num_added = Wrapping ( 3 ) ;
1560
- assert ! ( !q. prepare_kick( m ) ) ;
1558
+ assert ! ( !q. prepare_kick( ) ) ;
1561
1559
}
1562
1560
}
1563
1561
0 commit comments