Implement f16 and f128 cases in codegen_float_type (#3943)

See
#3069 (comment)
for a description of the issue.

Resolves #3069

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: carolynzech

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,
         }
     }
 

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();
+}