diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 9f97e7a0a5999..905e47bc60341 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -1331,11 +1331,11 @@ impl Expr {
     fn unop_return_type(op: UnaryOperator, arg: &Expr) -> Type {
         match op {
             Bitnot | BitReverse | Bswap | UnaryMinus => arg.typ.clone(),
-            CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.clone(),
+            CountLeadingZeros { .. } | CountTrailingZeros { .. } => Type::unsigned_int(32),
             ObjectSize | PointerObject => Type::size_t(),
             PointerOffset => Type::ssize_t(),
             IsDynamicObject | IsFinite | Not => Type::bool(),
-            Popcount => arg.typ.clone(),
+            Popcount => Type::unsigned_int(32),
         }
     }
     /// Private helper function to make unary operators
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 64c36dd76cfb7..df36189f46069 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -18,7 +18,7 @@ use rustc_middle::ty::{List, TypeFoldable};
 use rustc_smir::rustc_internal;
 use rustc_span::def_id::DefId;
 use rustc_target::abi::{
-    Abi::Vector, FieldIdx, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding,
+    Abi::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutS, Primitive, Size, TagEncoding,
     TyAndLayout, VariantIdx, Variants,
 };
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
@@ -1354,13 +1354,18 @@ impl<'tcx> GotocCtx<'tcx> {
                     }
                 }
             },
+            Primitive::Float(f) => self.codegen_float_type(f),
+            Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
+        }
+    }
 
-            Primitive::F32 => self.tcx.types.f32,
-            Primitive::F64 => self.tcx.types.f64,
+    pub fn codegen_float_type(&self, f: Float) -> Ty<'tcx> {
+        match f {
+            Float::F32 => self.tcx.types.f32,
+            Float::F64 => self.tcx.types.f64,
             // `F16` and `F128` are not yet handled.
             // Tracked here: <https://github.com/model-checking/kani/issues/3069>
-            Primitive::F16 | Primitive::F128 => unimplemented!(),
-            Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
+            Float::F16 | Float::F128 => unimplemented!(),
         }
     }
 
@@ -1672,7 +1677,7 @@ pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
 /// Extracts the pointee type if the given mir type is either a known smart pointer (Box, Rc, ..)
 /// or a regular pointer.
 pub fn std_pointee_type(mir_type: Ty) -> Option<Ty> {
-    mir_type.builtin_deref(true).map(|tm| tm.ty)
+    mir_type.builtin_deref(true)
 }
 
 /// This is a place holder function that should normalize the given type.
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 10b8c1275da6a..822f32631e0c2 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -16,8 +16,8 @@
 use rustc_hir::lang_items::LangItem;
 use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
+use rustc_middle::ty::TraitRef;
 use rustc_middle::ty::{ParamEnv, Ty, TyCtxt};
-use rustc_middle::ty::{TraitRef, TypeAndMut};
 use rustc_smir::rustc_internal;
 use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
 use stable_mir::Symbol;
@@ -263,5 +263,5 @@ fn custom_coerce_unsize_info<'tcx>(
 
 /// Extract pointee type from builtin pointer types.
 fn extract_pointee(tcx: TyCtxt<'_>, typ: TyStable) -> Option<Ty<'_>> {
-    rustc_internal::internal(tcx, typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
+    rustc_internal::internal(tcx, typ).builtin_deref(true)
 }
diff --git a/library/kani_macros/build.rs b/library/kani_macros/build.rs
new file mode 100644
index 0000000000000..c094cc0254c6c
--- /dev/null
+++ b/library/kani_macros/build.rs
@@ -0,0 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    // Make sure `kani_sysroot` is a recognized config
+    println!("cargo::rustc-check-cfg=cfg(kani_sysroot)");
+}
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index e571e9eaff4f6..021cbbf7a8fff 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-04-22"
+channel = "nightly-2024-05-14"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/expected/coroutines/as_parameter/main.rs b/tests/expected/coroutines/as_parameter/main.rs
index 7c0b9aed03736..33f56d04b2ae6 100644
--- a/tests/expected/coroutines/as_parameter/main.rs
+++ b/tests/expected/coroutines/as_parameter/main.rs
@@ -21,8 +21,11 @@ where
 
 #[kani::proof]
 fn main() {
-    foo(|| {
-        yield 1;
-        return 2;
-    });
+    foo(
+        #[coroutine]
+        || {
+            yield 1;
+            return 2;
+        },
+    );
 }
diff --git a/tests/expected/coroutines/main.rs b/tests/expected/coroutines/main.rs
index d94524c05d63d..9b76e6e4302ed 100644
--- a/tests/expected/coroutines/main.rs
+++ b/tests/expected/coroutines/main.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
@@ -10,7 +11,8 @@ use std::pin::Pin;
 #[kani::unwind(2)]
 fn main() {
     let val: bool = kani::any();
-    let mut coroutine = move || {
+    let mut coroutine = #[coroutine]
+    move || {
         let x = val;
         yield x;
         return !x;
diff --git a/tests/expected/coroutines/pin/main.rs b/tests/expected/coroutines/pin/main.rs
index 7d33005bb1380..fc97e57761e00 100644
--- a/tests/expected/coroutines/pin/main.rs
+++ b/tests/expected/coroutines/pin/main.rs
@@ -5,13 +5,15 @@
 // from https://github.com/model-checking/kani/issues/416
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
-    let mut coroutine = || {
+    let mut coroutine = #[coroutine]
+    || {
         yield 1;
         return true;
     };
diff --git a/tests/expected/intrinsics/ctpop-ice/ctpop_ice.rs b/tests/expected/intrinsics/ctpop-ice/ctpop_ice.rs
deleted file mode 100644
index ea11400e81613..0000000000000
--- a/tests/expected/intrinsics/ctpop-ice/ctpop_ice.rs
+++ /dev/null
@@ -1,14 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-//! Check that we correctly handle type mistmatch when the argument is a ZST type.
-//! The compiler crashes today: https://github.com/model-checking/kani/issues/2121
-
-#![feature(core_intrinsics)]
-use std::intrinsics::ctpop;
-
-// These shouldn't compile.
-#[kani::proof]
-pub fn check_zst_ctpop() {
-    let n = ctpop(());
-    assert!(n == ());
-}
diff --git a/tests/expected/intrinsics/ctpop-ice/expected b/tests/expected/intrinsics/ctpop-ice/expected
deleted file mode 100644
index 1ac989525f366..0000000000000
--- a/tests/expected/intrinsics/ctpop-ice/expected
+++ /dev/null
@@ -1,6 +0,0 @@
-error: Type check failed for intrinsic `ctpop`: Expected integer type, found ()
-   |
-12 |     let n = ctpop(());
-   |             ^^^^^^^^^
-
-error: aborting due to 1 previous error
\ No newline at end of file
diff --git a/tests/kani/Coroutines/main.rs b/tests/kani/Coroutines/main.rs
index 14cbeb426321c..e059305a6da20 100644
--- a/tests/kani/Coroutines/main.rs
+++ b/tests/kani/Coroutines/main.rs
@@ -4,6 +4,7 @@
 // This tests that coroutines work, even with a non-() resume type.
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
@@ -11,7 +12,8 @@ use std::pin::Pin;
 #[kani::proof]
 #[kani::unwind(3)]
 fn main() {
-    let mut add_one = |mut resume: u8| {
+    let mut add_one = #[coroutine]
+    |mut resume: u8| {
         loop {
             resume = yield resume.saturating_add(1);
         }
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/conditional-drop.rs b/tests/kani/Coroutines/rustc-coroutine-tests/conditional-drop.rs
index 81036a8f12388..a52f711fa52bd 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/conditional-drop.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/conditional-drop.rs
@@ -12,6 +12,7 @@
 //[nomiropt]compile-flags: -Z mir-opt-level=0
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::Coroutine;
 use std::pin::Pin;
@@ -41,7 +42,8 @@ fn main() {
 }
 
 fn t1() {
-    let mut a = || {
+    let mut a = #[coroutine]
+    || {
         let b = B;
         if test() {
             drop(b);
@@ -57,7 +59,8 @@ fn t1() {
 }
 
 fn t2() {
-    let mut a = || {
+    let mut a = #[coroutine]
+    || {
         let b = B;
         if test2() {
             drop(b);
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/control-flow.rs b/tests/kani/Coroutines/rustc-coroutine-tests/control-flow.rs
index 6e48b96e1d2af..af8d8a2250a4f 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/control-flow.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/control-flow.rs
@@ -35,32 +35,52 @@ where
 #[kani::proof]
 #[kani::unwind(16)]
 fn main() {
-    finish(1, || yield);
-    finish(8, || {
-        for _ in 0..8 {
-            yield;
-        }
-    });
-    finish(1, || {
-        if true {
-            yield;
-        } else {
-        }
-    });
-    finish(1, || {
-        if false {
-        } else {
-            yield;
-        }
-    });
-    finish(2, || {
-        if {
-            yield;
-            false
-        } {
-            yield;
-            panic!()
-        }
-        yield
-    });
+    finish(
+        1,
+        #[coroutine]
+        || yield,
+    );
+    finish(
+        8,
+        #[coroutine]
+        || {
+            for _ in 0..8 {
+                yield;
+            }
+        },
+    );
+    finish(
+        1,
+        #[coroutine]
+        || {
+            if true {
+                yield;
+            } else {
+            }
+        },
+    );
+    finish(
+        1,
+        #[coroutine]
+        || {
+            if false {
+            } else {
+                yield;
+            }
+        },
+    );
+    finish(
+        2,
+        #[coroutine]
+        || {
+            if {
+                yield;
+                false
+            } {
+                yield;
+                panic!()
+            }
+            yield
+        },
+    );
 }
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/env-drop.rs b/tests/kani/Coroutines/rustc-coroutine-tests/env-drop.rs
index a6420aca283b3..e1de81c9b0817 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/env-drop.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/env-drop.rs
@@ -12,6 +12,7 @@
 //[nomiropt]compile-flags: -Z mir-opt-level=0
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::Coroutine;
 use std::pin::Pin;
@@ -36,7 +37,8 @@ fn main() {
 
 fn t1() {
     let b = B;
-    let mut foo = || {
+    let mut foo = #[coroutine]
+    || {
         yield;
         drop(b);
     };
@@ -50,7 +52,8 @@ fn t1() {
 
 fn t2() {
     let b = B;
-    let mut foo = || {
+    let mut foo = #[coroutine]
+    || {
         yield b;
     };
 
@@ -63,7 +66,8 @@ fn t2() {
 
 fn t3() {
     let b = B;
-    let foo = || {
+    let foo = #[coroutine]
+    || {
         yield;
         drop(b);
     };
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/iterator-count.rs b/tests/kani/Coroutines/rustc-coroutine-tests/iterator-count.rs
index caa2efec216f6..8a9b26262e5de 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/iterator-count.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/iterator-count.rs
@@ -30,6 +30,7 @@ impl<T: Coroutine<(), Return = ()> + Unpin> Iterator for W<T> {
 }
 
 fn test() -> impl Coroutine<(), Return = (), Yield = u8> + Unpin {
+    #[coroutine]
     || {
         for i in 1..6 {
             yield i
@@ -43,6 +44,7 @@ fn main() {
     let end = 11;
 
     let closure_test = |start| {
+        #[coroutine]
         move || {
             for i in start..end {
                 yield i
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/live-upvar-across-yield.rs b/tests/kani/Coroutines/rustc-coroutine-tests/live-upvar-across-yield.rs
index 9bce8679464f4..d9aae2e953222 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/live-upvar-across-yield.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/live-upvar-across-yield.rs
@@ -9,6 +9,7 @@
 // run-pass
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::Coroutine;
 use std::pin::Pin;
@@ -16,7 +17,8 @@ use std::pin::Pin;
 #[kani::proof]
 fn main() {
     let b = |_| 3;
-    let mut a = || {
+    let mut a = #[coroutine]
+    || {
         b(yield);
     };
     Pin::new(&mut a).resume(());
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals-size.rs b/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals-size.rs
index d63d34427ca67..3c2b9dc16ae11 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals-size.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals-size.rs
@@ -41,6 +41,7 @@ impl Drop for Foo {
 }
 
 fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let first = Foo([0; FOO_SIZE]);
         let _second = first;
@@ -52,6 +53,7 @@ fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
 fn noop() {}
 
 fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let first = Foo([0; FOO_SIZE]);
         noop();
@@ -64,6 +66,7 @@ fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
 // Today we don't have NRVO (we allocate space for both `first` and `second`,)
 // but we can overlap `first` with `_third`.
 fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let first = Foo([0; FOO_SIZE]);
         yield;
@@ -75,6 +78,7 @@ fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
 }
 
 fn overlap_x_and_y() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let x = Foo([0; FOO_SIZE]);
         yield;
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals.rs b/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals.rs
index b3b6c4cc67677..6d54a54190e14 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals.rs
@@ -34,6 +34,7 @@ impl Drop for Foo {
 }
 
 fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let first = Foo([0; FOO_SIZE]);
         let _second = first;
@@ -45,6 +46,7 @@ fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
 fn noop() {}
 
 fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let first = Foo([0; FOO_SIZE]);
         noop();
@@ -57,6 +59,7 @@ fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
 // Today we don't have NRVO (we allocate space for both `first` and `second`,)
 // but we can overlap `first` with `_third`.
 fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let first = Foo([0; FOO_SIZE]);
         yield;
@@ -68,6 +71,7 @@ fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
 }
 
 fn overlap_x_and_y() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let x = Foo([0; FOO_SIZE]);
         yield;
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/nested-generators.rs b/tests/kani/Coroutines/rustc-coroutine-tests/nested-generators.rs
index 0d770380e2b99..8dfd8cdf065cc 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/nested-generators.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/nested-generators.rs
@@ -9,14 +9,17 @@
 // run-pass
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
-    let _coroutine = || {
-        let mut sub_coroutine = || {
+    let _coroutine = #[coroutine]
+    || {
+        let mut sub_coroutine = #[coroutine]
+        || {
             yield 2;
         };
 
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator-size.rs b/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator-size.rs
index 5de21166c3181..68b0a8589d3c1 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator-size.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator-size.rs
@@ -11,6 +11,7 @@
 // run-pass
 
 #![feature(coroutines)]
+#![feature(stmt_expr_attributes)]
 
 use std::mem::size_of_val;
 
@@ -19,7 +20,8 @@ fn take<T>(_: T) {}
 #[kani::proof]
 fn main() {
     let x = false;
-    let gen1 = || {
+    let gen1 = #[coroutine]
+    || {
         yield;
         take(x);
     };
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator.rs b/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator.rs
index 170a356fb3180..f882459910ece 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator.rs
@@ -11,6 +11,7 @@
 // run-pass
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
@@ -22,7 +23,8 @@ fn take<T>(_: T) {}
 #[kani::proof]
 fn main() {
     let x = false;
-    let mut gen1 = || {
+    let mut gen1 = #[coroutine]
+    || {
         yield;
         take(x);
     };
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals-size.rs b/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals-size.rs
index d22ed53f8b601..d7be6ba706f59 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals-size.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals-size.rs
@@ -9,10 +9,12 @@
 // run-pass
 
 #![feature(coroutines)]
+#![feature(stmt_expr_attributes)]
 
 #[kani::proof]
 fn main() {
-    let a = || {
+    let a = #[coroutine]
+    || {
         {
             let w: i32 = 4;
             yield;
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals.rs b/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals.rs
index 6033b2f06a999..56ba9d346d337 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals.rs
@@ -9,13 +9,15 @@
 // run-pass
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
-    let mut a = || {
+    let mut a = #[coroutine]
+    || {
         {
             let w: i32 = 4;
             yield;
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg-size.rs b/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg-size.rs
index f59ef260bcda9..958c3ea81d22e 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg-size.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg-size.rs
@@ -7,6 +7,7 @@
 // See GitHub history for details.
 
 #![feature(coroutines)]
+#![feature(stmt_expr_attributes)]
 
 // run-pass
 
@@ -15,7 +16,8 @@ use std::mem::size_of_val;
 #[kani::proof]
 fn main() {
     // Coroutine taking a `Copy`able resume arg.
-    let gen_copy = |mut x: usize| {
+    let gen_copy = #[coroutine]
+    |mut x: usize| {
         loop {
             drop(x);
             x = yield;
@@ -23,7 +25,8 @@ fn main() {
     };
 
     // Coroutine taking a non-`Copy` resume arg.
-    let gen_move = |mut x: Box<usize>| {
+    let gen_move = #[coroutine]
+    |mut x: Box<usize>| {
         loop {
             drop(x);
             x = yield;
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg.rs b/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg.rs
index 0c2c87f5eb2ed..c514ebf03eb77 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg.rs
@@ -7,6 +7,7 @@
 // See GitHub history for details.
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
@@ -18,7 +19,8 @@ use std::mem::size_of_val;
 #[kani::proof]
 fn main() {
     // Coroutine taking a `Copy`able resume arg.
-    let mut gen_copy = |mut x: usize| {
+    let mut gen_copy = #[coroutine]
+    |mut x: usize| {
         loop {
             drop(x);
             x = yield;
@@ -26,7 +28,8 @@ fn main() {
     };
 
     // Coroutine taking a non-`Copy` resume arg.
-    let mut gen_move = |mut x: Box<usize>| {
+    let mut gen_move = #[coroutine]
+    |mut x: Box<usize>| {
         loop {
             drop(x);
             x = yield;
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/resume-live-across-yield.rs b/tests/kani/Coroutines/rustc-coroutine-tests/resume-live-across-yield.rs
index 10d4d36223d5c..48c07a1a1fe87 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/resume-live-across-yield.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/resume-live-across-yield.rs
@@ -9,6 +9,7 @@
 // run-pass
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
@@ -28,7 +29,8 @@ impl Drop for Dropper {
 #[kani::proof]
 #[kani::unwind(16)]
 fn main() {
-    let mut g = |mut _d| {
+    let mut g = #[coroutine]
+    |mut _d| {
         _d = yield;
         _d
     };
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs b/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs
index 85c75bc8147d0..cc63b6b21186b 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs
@@ -12,6 +12,7 @@
 //[nomiropt]compile-flags: -Z mir-opt-level=0
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::fmt::Debug;
 use std::marker::Unpin;
@@ -61,7 +62,8 @@ fn expect_drops<T>(expected_drops: usize, f: impl FnOnce() -> T) -> T {
 #[kani::unwind(8)]
 fn main() {
     drain(
-        &mut |mut b| {
+        &mut #[coroutine]
+        |mut b| {
             while b != 0 {
                 b = yield (b + 1);
             }
@@ -70,21 +72,35 @@ fn main() {
         vec![(1, Yielded(2)), (-45, Yielded(-44)), (500, Yielded(501)), (0, Complete(-1))],
     );
 
-    expect_drops(2, || drain(&mut |a| yield a, vec![(DropMe, Yielded(DropMe))]));
+    expect_drops(2, || {
+        drain(
+            &mut #[coroutine]
+            |a| yield a,
+            vec![(DropMe, Yielded(DropMe))],
+        )
+    });
 
     expect_drops(6, || {
         drain(
-            &mut |a| yield yield a,
+            &mut #[coroutine]
+            |a| yield yield a,
             vec![(DropMe, Yielded(DropMe)), (DropMe, Yielded(DropMe)), (DropMe, Complete(DropMe))],
         )
     });
 
     #[allow(unreachable_code)]
-    expect_drops(2, || drain(&mut |a| yield return a, vec![(DropMe, Complete(DropMe))]));
+    expect_drops(2, || {
+        drain(
+            &mut #[coroutine]
+            |a| yield return a,
+            vec![(DropMe, Complete(DropMe))],
+        )
+    });
 
     expect_drops(2, || {
         drain(
-            &mut |a: DropMe| {
+            &mut #[coroutine]
+            |a: DropMe| {
                 if false { yield () } else { a }
             },
             vec![(DropMe, Complete(DropMe))],
@@ -94,7 +110,8 @@ fn main() {
     expect_drops(4, || {
         drain(
             #[allow(unused_assignments, unused_variables)]
-            &mut |mut a: DropMe| {
+            &mut #[coroutine]
+            |mut a: DropMe| {
                 a = yield;
                 a = yield;
                 a = yield;
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/smoke.rs b/tests/kani/Coroutines/rustc-coroutine-tests/smoke.rs
index 2b9aa40a06c02..c69513d00d995 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/smoke.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/smoke.rs
@@ -15,6 +15,7 @@
 // compile-flags: --test
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
@@ -22,7 +23,8 @@ use std::thread;
 
 #[kani::proof]
 fn simple() {
-    let mut foo = || {
+    let mut foo = #[coroutine]
+    || {
         if false {
             yield;
         }
@@ -38,7 +40,8 @@ fn simple() {
 #[kani::unwind(4)]
 fn return_capture() {
     let a = String::from("foo");
-    let mut foo = || {
+    let mut foo = #[coroutine]
+    || {
         if false {
             yield;
         }
@@ -53,7 +56,8 @@ fn return_capture() {
 
 #[kani::proof]
 fn simple_yield() {
-    let mut foo = || {
+    let mut foo = #[coroutine]
+    || {
         yield;
     };
 
@@ -71,7 +75,8 @@ fn simple_yield() {
 #[kani::unwind(4)]
 fn yield_capture() {
     let b = String::from("foo");
-    let mut foo = || {
+    let mut foo = #[coroutine]
+    || {
         yield b;
     };
 
@@ -88,7 +93,8 @@ fn yield_capture() {
 #[kani::proof]
 #[kani::unwind(4)]
 fn simple_yield_value() {
-    let mut foo = || {
+    let mut foo = #[coroutine]
+    || {
         yield String::from("bar");
         return String::from("foo");
     };
@@ -107,7 +113,8 @@ fn simple_yield_value() {
 #[kani::unwind(4)]
 fn return_after_yield() {
     let a = String::from("foo");
-    let mut foo = || {
+    let mut foo = #[coroutine]
+    || {
         yield;
         return a;
     };
@@ -124,43 +131,65 @@ fn return_after_yield() {
 
 // This test is useless for Kani
 fn send_and_sync() {
-    assert_send_sync(|| yield);
-    assert_send_sync(|| {
-        yield String::from("foo");
-    });
-    assert_send_sync(|| {
-        yield;
-        return String::from("foo");
-    });
+    assert_send_sync(
+        #[coroutine]
+        || yield,
+    );
+    assert_send_sync(
+        #[coroutine]
+        || {
+            yield String::from("foo");
+        },
+    );
+    assert_send_sync(
+        #[coroutine]
+        || {
+            yield;
+            return String::from("foo");
+        },
+    );
     let a = 3;
-    assert_send_sync(|| {
-        yield a;
-        return;
-    });
+    assert_send_sync(
+        #[coroutine]
+        || {
+            yield a;
+            return;
+        },
+    );
     let a = 3;
-    assert_send_sync(move || {
-        yield a;
-        return;
-    });
+    assert_send_sync(
+        #[coroutine]
+        move || {
+            yield a;
+            return;
+        },
+    );
     let a = String::from("a");
-    assert_send_sync(|| {
-        yield;
-        drop(a);
-        return;
-    });
+    assert_send_sync(
+        #[coroutine]
+        || {
+            yield;
+            drop(a);
+            return;
+        },
+    );
     let a = String::from("a");
-    assert_send_sync(move || {
-        yield;
-        drop(a);
-        return;
-    });
+    assert_send_sync(
+        #[coroutine]
+        move || {
+            yield;
+            drop(a);
+            return;
+        },
+    );
 
     fn assert_send_sync<T: Send + Sync>(_: T) {}
 }
 
 // Kani does not support threads, so we cannot run this test:
 fn send_over_threads() {
-    let mut foo = || yield;
+    let mut foo = #[coroutine]
+    || yield;
     thread::spawn(move || {
         match Pin::new(&mut foo).resume(()) {
             CoroutineState::Yielded(()) => {}
@@ -175,7 +204,8 @@ fn send_over_threads() {
     .unwrap();
 
     let a = String::from("a");
-    let mut foo = || yield a;
+    let mut foo = #[coroutine]
+    || yield a;
     thread::spawn(move || {
         match Pin::new(&mut foo).resume(()) {
             CoroutineState::Yielded(ref s) if *s == "a" => {}
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/static-generator.rs b/tests/kani/Coroutines/rustc-coroutine-tests/static-generator.rs
index 52f89438255a3..9b8ca468f9ee4 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/static-generator.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/static-generator.rs
@@ -9,13 +9,15 @@
 // run-pass
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
-    let mut coroutine = static || {
+    let mut coroutine = #[coroutine]
+    static || {
         let a = true;
         let b = &a;
         yield;
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/yield-in-box.rs b/tests/kani/Coroutines/rustc-coroutine-tests/yield-in-box.rs
index 5dbf580f5f579..79d6798855ffb 100644
--- a/tests/kani/Coroutines/rustc-coroutine-tests/yield-in-box.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/yield-in-box.rs
@@ -10,6 +10,7 @@
 // Test that box-statements with yields in them work.
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 use std::ops::Coroutine;
 use std::ops::CoroutineState;
 use std::pin::Pin;
@@ -17,6 +18,7 @@ use std::pin::Pin;
 #[kani::proof]
 fn main() {
     let x = 0i32;
+    #[coroutine]
     || {
         //~ WARN unused coroutine that must be used
         let y = 2u32;
@@ -28,7 +30,8 @@ fn main() {
         }
     };
 
-    let mut g = |_| Box::new(yield);
+    let mut g = #[coroutine]
+    |_| Box::new(yield);
     assert_eq!(Pin::new(&mut g).resume(1), CoroutineState::Yielded(()));
     assert_eq!(Pin::new(&mut g).resume(2), CoroutineState::Complete(Box::new(2)));
 }
diff --git a/tests/kani/Intrinsics/Count/ctlz.rs b/tests/kani/Intrinsics/Count/ctlz.rs
index 6c709137e5f48..9149b5bc8f54c 100644
--- a/tests/kani/Intrinsics/Count/ctlz.rs
+++ b/tests/kani/Intrinsics/Count/ctlz.rs
@@ -11,7 +11,7 @@ use std::intrinsics::{ctlz, ctlz_nonzero};
 // the same for any value
 macro_rules! test_ctlz {
     ( $fn_name:ident, $ty:ty ) => {
-        fn $fn_name(x: $ty) -> $ty {
+        fn $fn_name(x: $ty) -> u32 {
             let mut count = 0;
             let num_bits = <$ty>::BITS;
             for i in 0..num_bits {
diff --git a/tests/kani/Intrinsics/Count/ctpop.rs b/tests/kani/Intrinsics/Count/ctpop.rs
index d2eb972f83aa2..19d3ac4fd5a67 100644
--- a/tests/kani/Intrinsics/Count/ctpop.rs
+++ b/tests/kani/Intrinsics/Count/ctpop.rs
@@ -10,7 +10,7 @@ use std::intrinsics::ctpop;
 // the same for any value
 macro_rules! test_ctpop {
     ( $fn_name:ident, $ty:ty ) => {
-        fn $fn_name(x: $ty) -> $ty {
+        fn $fn_name(x: $ty) -> u32 {
             let mut count = 0;
             let num_bits = <$ty>::BITS;
             for i in 0..num_bits {
diff --git a/tests/kani/Intrinsics/Count/cttz.rs b/tests/kani/Intrinsics/Count/cttz.rs
index fa7c5f6a03e56..0429c6efce08c 100644
--- a/tests/kani/Intrinsics/Count/cttz.rs
+++ b/tests/kani/Intrinsics/Count/cttz.rs
@@ -11,7 +11,7 @@ use std::intrinsics::{cttz, cttz_nonzero};
 // the same for any value
 macro_rules! test_cttz {
     ( $fn_name:ident, $ty:ty ) => {
-        fn $fn_name(x: $ty) -> $ty {
+        fn $fn_name(x: $ty) -> u32 {
             let mut count = 0;
             let num_bits = <$ty>::BITS;
             for i in 0..num_bits {
diff --git a/tests/kani/Intrinsics/Rotate/rotate_left.rs b/tests/kani/Intrinsics/Rotate/rotate_left.rs
index d44ef1347745c..eac46f968b03d 100644
--- a/tests/kani/Intrinsics/Rotate/rotate_left.rs
+++ b/tests/kani/Intrinsics/Rotate/rotate_left.rs
@@ -24,7 +24,7 @@ macro_rules! test_rotate_left {
         let n: u32 = kani::any();
         // Limit `n` to `u8::MAX` to avoid overflows
         kani::assume(n <= u8::MAX as u32);
-        let y: $ty = rotate_left(x, n as $ty);
+        let y: $ty = rotate_left(x, n);
         // Check that the rotation is correct
         $fn_name(x, y, n);
         // Check that the stable version returns the same value
diff --git a/tests/kani/Intrinsics/Rotate/rotate_right.rs b/tests/kani/Intrinsics/Rotate/rotate_right.rs
index 584821e5784f2..9b88b1250b2fb 100644
--- a/tests/kani/Intrinsics/Rotate/rotate_right.rs
+++ b/tests/kani/Intrinsics/Rotate/rotate_right.rs
@@ -31,7 +31,7 @@ macro_rules! test_rotate_right {
         let n: u32 = kani::any();
         // Limit `n` to `u8::MAX` to avoid overflows
         kani::assume(n <= u8::MAX as u32);
-        let y: $ty = rotate_right(x, n as $ty);
+        let y: $ty = rotate_right(x, n);
         // Check that the rotation is correct
         $fn_name(x, y, n);
         // Check that the stable version returns the same value