From bb830fa0a02994cb5362722ceeb0fed5125d9c2e Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Mon, 17 Mar 2025 14:43:30 -0400
Subject: [PATCH] implement f16 and f128 cases in codegen_float_type

---
 .../src/codegen_cprover_gotoc/codegen/typ.rs      |  5 ++---
 tests/kani/FloatingPoint/main.rs                  | 15 +++++++++++++++
 2 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 48ce2ac7043d..84d2c52afba4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -1400,11 +1400,10 @@ impl<'tcx> GotocCtx<'tcx> {
 
     pub fn codegen_float_type(&self, f: Float) -> Ty<'tcx> {
         match f {
+            Float::F16 => self.tcx.types.f16,
             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>
-            Float::F16 | Float::F128 => unimplemented!(),
+            Float::F128 => self.tcx.types.f128,
         }
     }
 
diff --git a/tests/kani/FloatingPoint/main.rs b/tests/kani/FloatingPoint/main.rs
index f8ebccdac02a..38d801207594 100644
--- a/tests/kani/FloatingPoint/main.rs
+++ b/tests/kani/FloatingPoint/main.rs
@@ -3,6 +3,7 @@
 
 #![feature(f16)]
 #![feature(f128)]
+#![feature(repr_simd)]
 
 macro_rules! test_floats {
     ($ty:ty) => {
@@ -35,3 +36,17 @@ fn main() {
     test_floats!(f64);
     test_floats!(f128);
 }
+
+// Test that we can codegen floats when we hit them in codegen_float_type,
+// c.f. https://github.com/model-checking/kani/issues/3069#issuecomment-2730501056
+#[repr(simd)]
+struct f16x16([f16; 16]);
+
+fn make_float_array() -> f16x16 {
+    f16x16([1.0; 16])
+}
+
+#[kani::proof]
+fn make_float_array_harness() {
+    let _ = make_float_array();
+}