diff --git a/compiler/rustc_codegen_llvm/src/gotoc/place.rs b/compiler/rustc_codegen_llvm/src/gotoc/place.rs
index af31c24b9c7f..bfe4d0e33bfb 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/place.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/place.rs
@@ -199,22 +199,43 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    /// codegen for a local
-    pub fn codegen_local(&mut self, l: Local) -> Expr {
+    /// If a local is a function definition, ignore the local variable name and
+    /// generate a function call based on the def id.
+    ///
+    /// Note that this is finicky. A local might be a function definition or a
+    /// pointer to one. For example, the auto-generated code for Fn::call_once
+    /// uses a local FnDef to call the wrapped function, while the auto-generated
+    /// code for Fn::call and Fn::call_mut both use pointers to a FnDef.
+    /// In these cases, we need to generate an expression that references the
+    /// existing fndef rather than a named variable.
+    pub fn codegen_local_fndef(&mut self, l: Local) -> Option<Expr> {
         let t = self.local_ty(l);
         match t.kind() {
-            ty::FnDef(defid, substs) => {
-                // this is nasty. a local might have type FnDef, in which case, we should ignore
-                // the info about local completely.
-                self.codegen_fndef(*defid, substs, None)
-            }
-            _ => {
-                let vname = self.codegen_var_name(&l);
-                Expr::symbol_expression(vname, self.codegen_ty(t))
-            }
+            // A local that is itself a FnDef, like Fn::call_once
+            ty::FnDef(defid, substs) => Some(self.codegen_fndef(*defid, substs, None)),
+            // A local that is a pointer to a FnDef, like Fn::call and Fn::call_mut
+            ty::RawPtr(inner) => match inner.ty.kind() {
+                ty::FnDef(defid, substs) => {
+                    Some(self.codegen_fndef(*defid, substs, None).address_of())
+                }
+                _ => None,
+            },
+            _ => None,
         }
     }
 
+    /// Codegen for a local
+    pub fn codegen_local(&mut self, l: Local) -> Expr {
+        // Check if the local is a function definition (see comment above)
+        if let Some(fn_def) = self.codegen_local_fndef(l) {
+            return fn_def;
+        }
+
+        // Otherwise, simply look up the local by the var name.
+        let vname = self.codegen_var_name(&l);
+        Expr::symbol_expression(vname, self.codegen_ty(self.local_ty(l)))
+    }
+
     /// A projection is an operation that translates an lvalue to another lvalue.
     /// E.g. dereference, follow a field, etc.
     /// This function codegens a single step of a projection.
diff --git a/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs b/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs
index f638d11568db..c3a7f2cf90ef 100644
--- a/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs
+++ b/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs
@@ -7,9 +7,11 @@
 // called in the resulting CotoC code.
 // https://github.com/model-checking/rmc/issues/240
 
+include!("../../rmc-prelude.rs");
+
 fn main() {
     // Create a boxed once-callable closure
-    let f: Box<dyn FnOnce()> = Box::new(|x| {
+    let f: Box<dyn FnOnce(i32)> = Box::new(|x| {
         __VERIFIER_expect_fail(x == 2, "Wrong int");
     });
 
diff --git a/src/test/cbmc/DynTrait/dyn_fn_mut.rs b/src/test/cbmc/DynTrait/dyn_fn_mut.rs
new file mode 100644
index 000000000000..113a0445ea00
--- /dev/null
+++ b/src/test/cbmc/DynTrait/dyn_fn_mut.rs
@@ -0,0 +1,22 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we can pass a dyn FnMut pointer to a stand alone
+// function definition.
+
+fn takes_dyn_fun(mut fun: Box<dyn FnMut(&mut i32)>, x_ptr: &mut i32) {
+    fun(x_ptr)
+}
+
+pub fn mut_i32_ptr(x: &mut i32) {
+    *x = *x + 1;
+}
+
+fn main() {
+    let mut x = 1;
+    takes_dyn_fun(Box::new(&mut_i32_ptr), &mut x);
+    assert!(x == 2);
+
+    takes_dyn_fun(Box::new(&mut_i32_ptr), &mut x);
+    assert!(x == 3);
+}
diff --git a/src/test/cbmc/DynTrait/dyn_fn_mut_fail.rs b/src/test/cbmc/DynTrait/dyn_fn_mut_fail.rs
new file mode 100644
index 000000000000..37e2d13a38b4
--- /dev/null
+++ b/src/test/cbmc/DynTrait/dyn_fn_mut_fail.rs
@@ -0,0 +1,22 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we can pass a dyn FnMut pointer to a stand alone
+// function definition. Expected to fail because we are comparing
+// to an incorrect value.
+
+include!("../../rmc-prelude.rs");
+
+fn takes_dyn_fun(mut fun: Box<dyn FnMut(&mut i32)>, x_ptr: &mut i32) {
+    fun(x_ptr)
+}
+
+pub fn mut_i32_ptr(x: &mut i32) {
+    *x = *x + 1;
+}
+
+fn main() {
+    let mut x = 1;
+    takes_dyn_fun(Box::new(&mut_i32_ptr), &mut x);
+    __VERIFIER_expect_fail(x == 3, "Wrong x")
+}
diff --git a/src/test/cbmc/DynTrait/dyn_fn_once.rs b/src/test/cbmc/DynTrait/dyn_fn_once.rs
new file mode 100644
index 000000000000..cd77781fc0ba
--- /dev/null
+++ b/src/test/cbmc/DynTrait/dyn_fn_once.rs
@@ -0,0 +1,17 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we can pass a dyn FnOnce pointer to a stand alone
+// function definition.
+
+fn takes_dyn_fun(fun: Box<dyn FnOnce() -> u32>) -> u32 {
+    fun()
+}
+
+pub fn unit_to_u32() -> u32 {
+    5
+}
+
+fn main() {
+    assert!(takes_dyn_fun(Box::new(&unit_to_u32)) == 5)
+}
diff --git a/src/test/cbmc/DynTrait/dyn_fn_once_fail.rs b/src/test/cbmc/DynTrait/dyn_fn_once_fail.rs
new file mode 100644
index 000000000000..3015ee709231
--- /dev/null
+++ b/src/test/cbmc/DynTrait/dyn_fn_once_fail.rs
@@ -0,0 +1,20 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we can pass a dyn FnOnce pointer to a stand alone
+// function definition. Expected to fail because we are comparing
+// to an incorrect value.
+
+include!("../../rmc-prelude.rs");
+
+fn takes_dyn_fun(fun: Box<dyn FnOnce() -> u32>) -> u32 {
+    fun()
+}
+
+pub fn unit_to_u32() -> u32 {
+    5
+}
+
+fn main() {
+    __VERIFIER_expect_fail(takes_dyn_fun(Box::new(&unit_to_u32)) == 3, "Wrong u32")
+}
diff --git a/src/test/cbmc/DynTrait/dyn_fn_param_fail_fixme.rs b/src/test/cbmc/DynTrait/dyn_fn_param_fail.rs
similarity index 86%
rename from src/test/cbmc/DynTrait/dyn_fn_param_fail_fixme.rs
rename to src/test/cbmc/DynTrait/dyn_fn_param_fail.rs
index 601c55d4a26d..cf6c3d19df6e 100644
--- a/src/test/cbmc/DynTrait/dyn_fn_param_fail_fixme.rs
+++ b/src/test/cbmc/DynTrait/dyn_fn_param_fail.rs
@@ -2,9 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Check that we can pass a dyn function pointer to a stand alone
-// function definition. Inverted negative test.
+// function definition. Inverted negative test, expected to fail
+// all asserts.
 
-// FIXME https://github.com/model-checking/rmc/issues/240
 #![feature(ptr_metadata)]
 
 include!("../Helpers/vtable_utils_ignore.rs");