Codegen unimplemented for unsupported constant slices

See model-checking#1339 for more details.

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -105,8 +105,6 @@ impl<'tcx> GotocCtx<'tcx> {
                 ty::Slice(slice_ty) => {
                     if let Uint(UintTy::U8) = slice_ty.kind() {
                         // The case where we have a slice of u8 is easy enough: make an array of u8
-                        // TODO: Handle cases with larger int types by making an array of bytes,
-                        // then using byte-extract on it.
                         let slice =
                             data.inspect_with_uninit_and_ptr_outside_interpreter(start..end);
                         let vec_of_bytes: Vec<Expr> = slice
@@ -124,6 +122,16 @@ impl<'tcx> GotocCtx<'tcx> {
                             len_expr,
                             &self.symbol_table,
                         );
+                    } else {
+                        // TODO: Handle cases with other types such as tuples and larger integers.
+                        let loc = span.map_or(Location::none(), |s| self.codegen_span(s));
+                        let typ = self.codegen_ty(lit_ty);
+                        return self.codegen_unimplemented(
+                            "Constant slice value with 2+ bytes",
+                            typ,
+                            loc,
+                            "https://github.com/model-checking/kani/issues/1339",
+                        );
                     }
                 }
                 _ => {}