Split test into two depending on the platform

The same test currently succeeds for Linux but fails for MacOS, thus,
we split it into a regular test and a fixme test.

Author: celinval

tests/kani/SizeAndAlignOfDst/main_assert.rs

@@ -1,58 +1,58 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// The original harness takes too long so we introduced a simplified version to run in CI.
-// kani-flags: --harness simplified
 
 //! This is a regression test for size_and_align_of_dst computing the
 //! size and alignment of a dynamically-sized type like
 //! Arc<Mutex<dyn Subscriber>>.
-//! We added a simplified version of the original harness from:
 //! <https://github.com/model-checking/kani/issues/426>
-//! This currently fails due to
-//! <https://github.com/model-checking/kani/issues/1781>
 
-use std::sync::Arc;
-use std::sync::Mutex;
-
-pub trait Subscriber {
-    fn process(&self);
-    fn increment(&mut self);
-    fn get(&self) -> u32;
-}
-
-struct DummySubscriber {
-    val: u32,
-}
+/// This test fails on macos but not in other platforms.
+/// Thus only enable it for platforms where this shall succeed.
+#[cfg(not(target_os = "macos"))]
+mod not_macos {
+    use std::sync::Arc;
+    use std::sync::Mutex;
+
+    pub trait Subscriber {
+        fn process(&self);
+        fn increment(&mut self);
+        fn get(&self) -> u32;
+    }
 
-impl DummySubscriber {
-    fn new() -> Self {
-        DummySubscriber { val: 0 }
+    struct DummySubscriber {
+        val: u32,
     }
-}
 
-impl Subscriber for DummySubscriber {
-    fn process(&self) {}
-    fn increment(&mut self) {
-        self.val = self.val + 1;
+    impl DummySubscriber {
+        fn new() -> Self {
+            DummySubscriber { val: 0 }
+        }
     }
-    fn get(&self) -> u32 {
-        self.val
+
+    impl Subscriber for DummySubscriber {
+        fn process(&self) {}
+        fn increment(&mut self) {
+            self.val = self.val + 1;
+        }
+        fn get(&self) -> u32 {
+            self.val
+        }
     }
-}
 
-#[kani::proof]
-#[kani::unwind(2)]
-fn simplified() {
-    let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
-    let data = s.lock().unwrap();
-    assert!(data.get() == 0);
-}
+    #[kani::proof]
+    #[kani::unwind(2)]
+    fn simplified() {
+        let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
+        let data = s.lock().unwrap();
+        assert!(data.get() == 0);
+    }
 
-#[kani::proof]
-#[kani::unwind(1)]
-fn original() {
-    let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
-    let mut data = s.lock().unwrap();
-    data.increment();
-    assert!(data.get() == 1);
+    #[kani::proof]
+    #[kani::unwind(1)]
+    fn original() {
+        let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
+        let mut data = s.lock().unwrap();
+        data.increment();
+        assert!(data.get() == 1);
+    }
 }

tests/kani/SizeAndAlignOfDst/main_assert_fixme.rs

@@ -0,0 +1,71 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// The original harness takes too long so we introduced a simplified version to run in CI.
+// kani-flags: --harness simplified
+
+//! This is a regression test for size_and_align_of_dst computing the
+//! size and alignment of a dynamically-sized type like
+//! Arc<Mutex<dyn Subscriber>>.
+//! We added a simplified version of the original harness from:
+//! <https://github.com/model-checking/kani/issues/426>
+//! This currently fails on MacOS instances due to unsupported foreign function:
+//! `pthread_mutexattr_init`.
+
+#[cfg(target_os = "macos")]
+mod macos {
+    use std::sync::Arc;
+    use std::sync::Mutex;
+
+    pub trait Subscriber {
+        fn process(&self);
+        fn increment(&mut self);
+        fn get(&self) -> u32;
+    }
+
+    struct DummySubscriber {
+        val: u32,
+    }
+
+    impl DummySubscriber {
+        fn new() -> Self {
+            DummySubscriber { val: 0 }
+        }
+    }
+
+    impl Subscriber for DummySubscriber {
+        fn process(&self) {}
+        fn increment(&mut self) {
+            self.val = self.val + 1;
+        }
+        fn get(&self) -> u32 {
+            self.val
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(2)]
+    fn simplified() {
+        let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
+        let data = s.lock().unwrap();
+        assert!(data.get() == 0);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(1)]
+    fn original() {
+        let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
+        let mut data = s.lock().unwrap();
+        data.increment();
+        assert!(data.get() == 1);
+    }
+}
+
+#[cfg(not(target_os = "macos"))]
+mod not_macos {
+    /// Since this is a fixme test, it must also fail in other platforms.
+    /// Remove this once we fix the issue above.
+    #[kani::proof]
+    fn fail() {
+        assert!(false);
+    }
+}