#3306 missed:

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

Lines 1405 to 1407 in ce89f61

    
           // `F16` and `F128` are not yet handled. 
        
           // Tracked here: <https://github.com/model-checking/kani/issues/3069> 
        
           Float::F16 | Float::F128 => unimplemented!(),

which were added to TyCtxt in
rust-lang/rust@e3f63d9#diff-0c8c9cf0c0f8cda43eb64bbe5ef63c3239b0cf25901587b3c1f2b1d97a7e8441R340

Here's a minimal reproducer for this crash:

#![feature(f16)]
#![feature(repr_simd)]

#[repr(simd)]
struct f16x16([f16; 16]);

fn foo() -> f16x16 {
    f16x16([1.0; 16])
}

(The simd layout ensures we get to this line:

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

Line 1481 in ce89f61

let rust_type = self.codegen_prim_typ(prim_type);

and thereby hit the ICE).

	// `F16` and `F128` are not yet handled.
	// Tracked here: <https://github.com/model-checking/kani/issues/3069>
	Float::F16 \| Float::F128 => unimplemented!(),

Handle new F16 and F128 types #3069

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Handle new `F16` and `F128` types #3069