Kani cannot handle constant slice with element type different than U8.

[celinval]

I tried compiling the std crate after updating the toolchain to 2022-07-05. I got the following error while trying code generation of the std library using the following command line invocation:

./scripts/std-lib-regression.sh

with Kani version: 0.5

I expected to see this happen: Finished Kani codegen for the Rust standard library successfully...

Instead, this happened:

thread 'rustc' panicked at 'not implemented:                                                                                                                                                                
v Slice { data: Allocation { bytes: [0, 1, 3, 5, 5, 6, 6, 2, 7, 6, 8, 7, 9, 17, 10, 28, 11, 25, 12, 26, 13, 16, 14, 13, 15, 4, 16, 3, 18, 18, 19, 9, 22, 1, 23, 4, 24, 1, 25, 3, 26, 7, 27, 1, 28, 2, 31, 22
, 32, 3, 43, 3, 45, 11, 46, 1, 48, 3, 49, 2, 50, 1, 167, 2, 169, 2, 170, 4, 171, 8, 250, 2, 251, 5, 253, 2, 254, 3, 255, 9], relocations: Relocations(SortedMap { data: [] }), init_mask: InitMask { blocks:
 [18446744073709551615, 65535], len: Size(80 bytes) }, align: Align(128 bytes), mutability: Not, extra: () }, start: 0, end: 40 }                                                                           
lit_ty &[(u8, u8)]                                                                                                                                                                                          
span Some(/rustup/toolchains/nightly-2022-07-05-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/unicode/printable.rs:50:22: 50:34 (#0))', kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:132:9 

[Kani] current codegen item: codegen_function: unicode::printable::is_printable                                                                                                                             
_ZN4core7unicode9printable12is_printable17h26e35c8ac4e6d19aE                                                                                                                                                
[Kani] current codegen location: Loc { file: "/rustup/toolchains/nightly-2022-07-05-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/unicode/printable.rs", func
tion: None, line: 39, col: Some(1) } 

[danielsn]

This line also worries me https://github.com/model-checking/kani/blob/main/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs#L128

[zhassan-aws]

This is likely no longer an issue given that Kani is regularly run on the standard library in https://github.com/model-checking/verify-rust-std/