Fix comments and tests

Author: Patrick-6

src/concurrency/genmc/intercept.rs

@@ -27,7 +27,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             .expect("This function should only be called in GenMC mode.");
 
         let get_mutex_call_infos = || {
-            // assert!(!args.is_empty());
             assert_eq!(args.len(), 1);
             let arg = this.copy_fn_arg(&args[0]);
             let addr = this.read_target_usize(&arg)?;

tests/genmc/fail/intercept/mutex_deadlock.rs

@@ -1,7 +1,8 @@
 //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
 //@error-in-other-file: unsupported operation
 
-// TODO
+// Test that we can detect a deadlock involving `std::sync::Mutex` in GenMC mode.
+// FIXME(genmc): The error message for such deadlocks is currently not good, it does not show both involved lock call locations.
 
 #![no_main]
 #![feature(abort_unwind)]

tests/genmc/pass/intercept/mutex_simple.rs

@@ -54,21 +54,23 @@ fn main_() {
         assert!(LOCK.try_lock().is_ok()); // Trying to lock now should *not* fail since the lock is not held.
     }
 
-    let ids = [
-        spawn_pthread_closure(|| {
-            for _ in 0..REPS {
-                let mut guard = LOCK.lock().unwrap();
-                guard[0] += 2;
-            }
-        }),
-        spawn_pthread_closure(|| {
-            for _ in 0..REPS {
-                let mut guard = LOCK.lock().unwrap();
-                guard[0] += 4;
-            }
-        }),
-    ];
-    unsafe { join_pthreads(ids) };
+    unsafe {
+        let ids = [
+            spawn_pthread_closure(|| {
+                for _ in 0..REPS {
+                    let mut guard = LOCK.lock().unwrap();
+                    guard[0] += 2;
+                }
+            }),
+            spawn_pthread_closure(|| {
+                for _ in 0..REPS {
+                    let mut guard = LOCK.lock().unwrap();
+                    guard[0] += 4;
+                }
+            }),
+        ];
+        join_pthreads(ids);
+    }
 
     let guard = LOCK.lock().unwrap();
     assert!(guard[0] == REPS * 6); // Due to locking, all increments should be visible in every execution.