| Category | Count |
|---|
| bug: verification error could not be backtranslated (no crash) | 500 |
| unsupported: unsizing with unsupported types (no crash) | 253 |
| unsupported: closure rvalue might be reached (no crash) | 171 |
| bug: duplicate identifier in consistency check (no crash) | 152 |
| bug: ReVar from outer InferCtxt in try_normalize | 98 |
| unsupported (pcg): call with unsafe ptr with nested lifetime | 89 |
| unsupported: nested references in promoted constants | 57 |
| unsupported (pcg): dereferencing unsafe pointers | 57 |
| unsupported: &raw mut/const rvalue might be reached (no crash) | 55 |
| unsupported: passing functions into other functions | 47 |
| internal error: entered unreachable code: FieldsShape::offset: `Primitive`s have no fields | 24 |
| unsupported: c string literals | 24 |
| unsupported: coroutine types | 23 |
| unsupported: binary operation with one operand of pointer type | 19 |
| success | 16 |
| not yet implemented | 13 |
| unsupported: bitwise operations | 11 |
| bug: invalid arguments to domain function in consistency check (no crash) | 9 |
| cannot unfold array type without index | 8 |
| not yet implemented: cast kind PtrToPtr | 7 |
| bug: invalid identifier in consistency check (no crash) | 6 |
| `ref_to_mplace` called on non-ptr type | 6 |
| unsupported: implicit mut-to-const pointer coercions | 5 |
| called `Result::unwrap()` on an `Err` value: InterpErrorInfo(InterpErrorInfoInner { kind: MachineStop(ConstAccessesMutGlobal), backtrace: InterpErrorBacktrace { backtrace: None } }) | 4 |
| not yet implemented: cast kind PointerCoercion(ClosureFnPointer(Safe), Implicit) | 4 |
| internal error: entered unreachable code | 3 |
| not yet implemented: cast kind PointerExposeProvenance | 3 |
| called `Result::unwrap()` on an `Err` value: Protocol("Connection reset without closing handshake") | 2 |
| bug: index out of bounds in GenericParams::map_index | 2 |
| unsupported (pcg): move unsafe ptr with nested lifetime | 2 |
| offending pos id is missing for error VerificationError { full_id: "application.precondition:insufficient.permission", pos_id: None, offending_pos_id: None, reason_pos_id: None, message: "Precondition of function p_Int_i32_snap might not hold. There might be insufficient permission to access p_Int_i32(s_Option_1_field_0(_1p, s_Int_i32_type())) (<no position>)\n", counterexample: None } | 2 |
| not yet implemented: cast kind PointerCoercion(ReifyFnPointer, Implicit) | 2 |
| Expected a pointer: InterpErrorInfo(InterpErrorInfoInner { kind: UndefinedBehavior(ScalarSizeMismatch(ScalarSizeMismatch { target_size: 8, data_size: 4 })), backtrace: InterpErrorBacktrace { backtrace: None } }) | 2 |
| not yet implemented: const too generic | 2 |
| expected opaque (was TyData { data: TyUsePureRef { snapshot: s_Slice, args: GArgsTy { ty_args: [s_Int_i32_type()], const_args: [] }, ty_pure_ref: TyPureRef { domain: DomainIdn { idn: ViperIdent("s_Slice"), params: 0, _p: PhantomData<vir::type::Snap> }, unreachable_to_snap: FunctionIdn { idn: ViperIdent("s_Slice_unreachable"), args: ([Type], []), result_ty: s_Slice, debug_info: DebugInfo(PhantomData<&()>) } } }, specifics: Array(ArrayData { data: TyUsePureArrayData { caster: Casters(Casters { cast: GArgCasters { make_generic: FunctionIdn { idn: ViperIdent("make_generic_s_Int_i32"), args: (s_Int_i32, [], []), result_ty: s_Param, debug_info: DebugInfo(PhantomData<&()>) }, make_concrete: FunctionIdn { idn: ViperIdent("make_concrete_s_Int_i32"), args: (s_Param, [], []), result_ty: s_Int_i32, debug_info: DebugInfo(PhantomData<&()>) } }, ty_args: GArgsTy { ty_args: [], const_args: [] } }), args: GArgsTy { ty_args: [s_Int_i32_type()], const_args: [] }, pure: TyPureArrayData { index_access: FunctionIdn { idn: ViperIdent("s_Slice_index"), args: (s_Slice, Int), result_ty: s_Param, debug_info: DebugInfo(PhantomData<&()>) }, ref_to_index_ref: FunctionIdn { idn: ViperIdent("s_Slice_index_ref"), args: (Ref, Int, [Type], []), result_ty: Ref, debug_info: DebugInfo(PhantomData<&()>) }, len: FunctionIdn { idn: ViperIdent("s_Slice_len"), args: s_Slice, result_ty: Int, debug_info: DebugInfo(PhantomData<&()>) } } }, slice: true }) }) | 2 |
| not yet implemented: cast kind PointerCoercion(ReifyFnPointer, AsCast) | 2 |
| offending pos id is missing for error VerificationError { full_id: "call.precondition:insufficient.permission", pos_id: None, offending_pos_id: None, reason_pos_id: None, message: "The precondition of method make_concrete_String might not hold. There might be insufficient permission to access p_Param(get_s_Ref_mutable_s_Ref_mutable_0(p_Ref_mutable_snap(_7p, s_String_type())), s_String_type()) (<no position>)\n", counterexample: None } | 1 |
| PCG Assertion Failed : [main::debuginfo] capabilities.get(RETURN_PLACE.into(), ctxt).unwrap() == | 1 |
| not yet implemented: cast kind PointerWithExposedProvenance | 1 |
| Box<dyn Any> | 1 |
| not yet implemented: cast kind FloatToInt | 1 |
| PCG Assertion Failed : [main::set] capabilities.get(RETURN_PLACE.into(), ctxt).unwrap() == | 1 |
| not yet implemented: cast kind IntToFloat | 1 |
| expected structlike or enumlike type | 1 |