Skip to content

kani-compiler panic on unimplemented scalar #2099

@tedinski

Description

@tedinski

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:

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.[F] CrashKani crashed

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions