From 71b1188cc8beba8ea4029f0ea4da6711a80339d7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 5 Jul 2022 23:16:45 -0700 Subject: [PATCH] Codegen unimplemented for unsupported constant slices See https://github.com/model-checking/kani/issues/1339 for more details. --- .../src/codegen_cprover_gotoc/codegen/operand.rs | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index da7c953c493c..15975bf1ee54 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/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 = 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", + ); } } _ => {}