Reproduction:
git clone https://github.com/bitflags/bitflags
cd bitflags
RUST_BACKTRACE=1 cargo kani --enable-unstable --only-codegen assess
Result:
thread '<unnamed>' panicked at 'not implemented', kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:419:18
stack backtrace:
3: kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_scalar
at /home/ubuntu/rmc/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:419:18
4: kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_single_variant_single_field
at /home/ubuntu/rmc/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:438:22
The code in question is a remaining raw unimplemented in codegen_scalar:
Reproduction:
Result:
The code in question is a remaining raw
unimplementedincodegen_scalar:kani/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Line 419 in 5680dac