@@ -12,7 +12,7 @@ use crate::data_structures::petri_net_interface::{PetriNet, TransitionRef};
12
12
use crate :: naming:: condvar:: wait_transition_labels;
13
13
use crate :: translator:: function_call:: FunctionPlaces ;
14
14
use crate :: translator:: mir_function:: Memory ;
15
- use crate :: utils:: extract_nth_argument ;
15
+ use crate :: utils:: extract_nth_argument_as_place ;
16
16
use log:: debug;
17
17
18
18
#[ derive( Default ) ]
@@ -76,13 +76,15 @@ impl CondvarManager {
76
76
memory : & mut Memory < ' tcx > ,
77
77
) {
78
78
// Retrieve the lock guard from the local variable passed to the function as an argument.
79
- let lock_guard = extract_nth_argument ( args, 1 ) ;
79
+ let lock_guard = extract_nth_argument_as_place ( args, 1 )
80
+ . expect ( "BUG: `std::sync::Condvar::wait` should receive the first argument as a place" ) ;
80
81
let mutex_ref = memory. get_linked_lock_guard ( & lock_guard) ;
81
82
// Unlock the mutex when waiting, lock it when the waiting ends.
82
83
mutex_manager. add_unlock_guard ( * mutex_ref, & wait_transitions. 0 , net) ;
83
84
mutex_manager. add_lock_guard ( * mutex_ref, & wait_transitions. 1 , net) ;
84
85
// Retrieve the condvar from the local variable passed to the function as an argument.
85
- let self_ref = extract_nth_argument ( args, 0 ) ;
86
+ let self_ref = extract_nth_argument_as_place ( args, 0 )
87
+ . expect ( "BUG: `std::sync::Condvar::wait` should receive the self reference as a place" ) ;
86
88
let condvar_ref = memory. get_linked_condvar ( & self_ref) ;
87
89
self . link_to_wait_call ( * condvar_ref, wait_transitions, net) ;
88
90
// The return value contains the lock guard passed to the function. Link the local variable to it.
@@ -101,7 +103,9 @@ impl CondvarManager {
101
103
memory : & mut Memory < ' tcx > ,
102
104
) {
103
105
// Retrieve the condvar from the local variable passed to the function as an argument.
104
- let self_ref = extract_nth_argument ( args, 0 ) ;
106
+ let self_ref = extract_nth_argument_as_place ( args, 0 ) . expect (
107
+ "BUG: `std::sync::Condvar::notify_one` should receive the self reference as a place" ,
108
+ ) ;
105
109
let condvar_ref = memory. get_linked_condvar ( & self_ref) ;
106
110
self . link_to_notify_one_call ( * condvar_ref, notify_one_transition, net) ;
107
111
}
0 commit comments