Prusti Analysis

Database	Total	Success	Fail	Timeout
prusti-20260227-115713-f74843625.db	3379	967	2392	20
prusti-20260304-165534-d23d93192.db	3379	964	2391	24
prusti-20260305-202754-937425f70.db	3379	968	2388	23
prusti-20260306-164218-cd5e443f3.db	3379	975	2380	24
prusti-20260309-112628-c8b922649.db	3379	979	2376	24
prusti-20260309-120329-3db661888.db	3379	990	2365	24
prusti-20260309-122840-ad11284f6.db	3379	992	2362	25
prusti-20260309-175527-9eba9fcdc.db	3379	982	2372	25
prusti-20260317-151414-d20ecc48c.db	3379	993	2361	25
prusti-20260320-130143-1336a4b80.db	3379	1003	2351	25
prusti-20260320-162729-4ee0f8d94.db	3379	429	2930	20
prusti-20260323-121434-7d1dded3b.db	3379	429	2930	20
prusti-20260323-125921-08b08c532.db	3379	435	2897	47
prusti-20260330-142143-52e9f08d2.db	3379	472	2861	46
prusti-20260402-002524-e1d5e6c24.db	3379	474	2859	46
prusti-20260410-212618-bd3a77aef.db	3379	1605	1721	53
prusti-20260411-002735-8d9c868d0.db	3379	1605	1721	53
prusti-20260417-100008-5cd3f71f8.db	3379	1605	1721	53
prusti-20260426-174735-3d9ad6e85.db	3379	1605	1721	53
prusti-20260427-162946-c69ced09f.db	3379	1608	1718	53
prusti-20260428-154632-6e19cc770.db	3379	1608	1718	53
prusti-20260430-161753-9945d1347.db	3379	1608	1718	53
prusti-20260505-163045-ad5e5b44b.db	3379	1612	1714	53
prusti-20260505-185055-29fff11aa.db	3379	1612	1714	53
prusti-20260511-125024-939160592.db	3379	1612	1714	53
prusti-20260513-142116-0ffb80180.db	3379	1638	1688	53
prusti-fix-missing-substitution-in-apply-wands-20260515-162448-aaf0046ee.db	3379	1652	1674	53
prusti-fix-revar-from-outer-inferctxt-in-try-normalize-20260514-092649-0ca6d84a4.db	3379	1638	1688	53

Category	prusti-20260227-115713-f74843625	prusti-20260304-165534-d23d93192	prusti-20260305-202754-937425f70	prusti-20260306-164218-cd5e443f3	prusti-20260309-112628-c8b922649	prusti-20260309-120329-3db661888	prusti-20260309-122840-ad11284f6	prusti-20260309-175527-9eba9fcdc	prusti-20260317-151414-d20ecc48c	prusti-20260320-130143-1336a4b80	prusti-20260320-162729-4ee0f8d94	prusti-20260323-121434-7d1dded3b	prusti-20260323-125921-08b08c532	prusti-20260330-142143-52e9f08d2	prusti-20260402-002524-e1d5e6c24	prusti-20260410-212618-bd3a77aef	prusti-20260411-002735-8d9c868d0	prusti-20260417-100008-5cd3f71f8	prusti-20260426-174735-3d9ad6e85	prusti-20260427-162946-c69ced09f	prusti-20260428-154632-6e19cc770	prusti-20260430-161753-9945d1347	prusti-20260505-163045-ad5e5b44b	prusti-20260505-185055-29fff11aa	prusti-20260511-125024-939160592	prusti-20260513-142116-0ffb80180	prusti-fix-missing-substitution-in-apply-wands-20260515-162448-aaf0046ee	prusti-fix-revar-from-outer-inferctxt-in-try-normalize-20260514-092649-0ca6d84a4
bug: verification error could not be backtranslated (no crash)	8	66	73	81	80	82	85	85	85	85	20	20	20	24	22	368	368	368	402	407	408	360	360	360	360	382	500	409
unsupported: unsizing with unsupported types (no crash)	212	212	217	217	217	222	222	217	265	270	267	267	242	249	249	328	328	328	253	262	263	302	304	304	304	250	253	254
bug: local variable not found in consistency check (no crash)	0	0	0	24	23	35	35	25	26	36	14	14	14	14	14	152	152	152	156	156	159	159	159	159	159	159	0	180
bug: duplicate identifier in consistency check (no crash)	14	16	16	9	9	10	10	9	12	13	7	7	7	9	9	140	140	140	143	143	157	157	157	157	157	157	152	169
unsupported: closure rvalue might be reached (no crash)	18	20	20	27	28	33	33	28	31	36	10	10	10	13	13	139	139	139	144	146	148	154	154	154	154	154	171	159
unsupported (pcg): call with unsafe ptr with nested lifetime	2	2	2	2	2	12	12	2	3	14	13	13	13	16	16	17	17	17	19	19	89	89	89	89	89	89	89	90
bug: ReVar from outer InferCtxt in try_normalize	20	21	31	32	32	63	63	36	36	63	58	58	55	58	58	71	71	71	72	72	81	81	81	81	82	82	98	0
unsupported: nested references in promoted constants	0	0	0	0	0	0	0	0	0	0	0	0	0	7	7	52	52	52	52	52	60	60	60	60	60	60	57	63
unsupported (pcg): dereferencing unsafe pointers	47	47	48	49	49	49	49	49	49	49	47	47	45	47	47	57	57	57	57	57	57	57	57	57	57	57	57	57
unsupported: &raw mut/const rvalue might be reached (no crash)	42	42	42	42	42	42	42	42	42	42	22	22	22	22	22	50	50	50	52	52	52	55	55	55	55	55	55	55
unsupported: passing functions into other functions	19	22	26	26	26	27	27	26	27	28	28	28	28	34	34	46	46	46	47	47	47	47	47	47	47	47	47	47
internal error: entered unreachable code: FieldsShape::offset: `Primitive`s have no fields	0	0	0	0	0	0	0	0	0	0	0	0	0	9	9	24	24	24	24	24	24	24	24	24	24	24	24	24
unsupported: c string literals	21	21	21	21	21	21	21	21	21	21	21	21	20	22	22	24	24	24	24	24	24	24	24	24	24	24	24	24
unsupported: coroutine types	18	18	18	18	18	19	19	19	23	23	22	22	20	20	20	23	23	23	23	23	23	23	23	23	23	23	23	23
unsupported: binary operation with one operand of pointer type	17	17	17	17	17	17	17	17	17	17	11	11	9	11	11	19	19	19	19	19	19	19	19	19	19	19	19	19
not yet implemented	4	4	4	4	4	4	4	4	4	4	4	4	4	13	13	13	13	13	13	13	13	13	13	13	13	13	13	13
unsupported: bitwise operations	7	7	7	7	7	7	7	7	7	7	7	7	7	7	7	7	7	7	11	11	11	11	11	11	11	11	11	11
bug: invalid arguments to domain function in consistency check (no crash)	9	9	9	9	9	9	9	9	9	9	0	0	0	0	0	9	9	9	9	9	9	9	9	9	9	9	9	9
cannot unfold array type without index	1	1	3	3	3	3	3	3	3	3	3	3	1	1	1	8	8	8	8	8	8	8	8	8	8	8	8	9
success	3	4	4	4	4	4	4	4	4	4	2	2	2	2	2	6	6	6	6	6	6	6	6	6	6	8	16	8
not yet implemented: cast kind PtrToPtr	9	9	9	9	9	9	9	9	9	9	9	9	7	7	7	7	7	7	7	7	7	7	7	7	7	7	7	7
bug: invalid identifier in consistency check (no crash)	2	7	7	8	8	8	2	2	3	3	2	2	2	2	2	5	5	5	19	0	0	0	0	0	0	6	6	6
`ref_to_mplace` called on non-ptr type	0	0	0	0	0	0	0	0	0	0	0	0	0	1	1	6	6	6	6	6	6	6	6	6	6	6	6	6
unsupported: implicit mut-to-const pointer coercions	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5	5
not yet implemented: cast kind PointerExposeProvenance	3	3	3	3	3	3	3	3	3	3	3	3	3	3	3	4	4	4	4	4	4	4	4	4	4	4	3	4
called `Result::unwrap()` on an `Err` value: InterpErrorInfo(InterpErrorInfoInner { kind: MachineStop(ConstAccessesMutGlobal), backtrace: InterpErrorBacktrace { backtrace: None } })	0	0	0	0	0	0	0	0	0	0	0	0	0	3	3	3	3	3	3	3	4	4	4	4	4	4	4	4
not yet implemented: cast kind PointerCoercion(ClosureFnPointer(Safe), Implicit)	3	3	3	3	3	3	3	3	4	4	4	4	4	4	4	4	4	4	4	4	4	4	4	4	4	4	4	4
internal error: entered unreachable code	3	3	3	3	3	3	3	3	3	3	2	2	2	2	2	3	3	3	3	3	3	3	3	3	3	3	3	3
not yet implemented: const too generic	1	1	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2
not yet implemented: cast kind PointerCoercion(ReifyFnPointer, AsCast)	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2
Expected a pointer: InterpErrorInfo(InterpErrorInfoInner { kind: UndefinedBehavior(ScalarSizeMismatch(ScalarSizeMismatch { target_size: 8, data_size: 4 })), backtrace: InterpErrorBacktrace { backtrace: None } })	0	0	0	0	0	0	0	0	0	0	0	0	0	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2
unsupported (pcg): move unsafe ptr with nested lifetime	0	0	0	0	0	0	0	0	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2
bug: index out of bounds in GenericParams::map_index	0	4	4	4	4	4	4	4	4	4	3	3	3	3	3	6	6	6	8	8	8	8	2	2	2	2	2	2
called `Result::unwrap()` on an `Err` value: Protocol("Connection reset without closing handshake")	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	1	1	1	2	2	2	2	2	2	2	2	2	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 }) })	0	0	0	0	0	0	0	0	0	0	0	0	0	2	2	2	2	2	2	2	2	2	2	2	2	2	2	3
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	2	2	2	2	2	2	2	2	2	0	0	0	0	0	2	2	2	2	2	2	2	2	2	2	2	2	2
not yet implemented: cast kind PointerCoercion(ReifyFnPointer, Implicit)	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2	2
PCG Assertion Failed : [main::debuginfo] capabilities.get(RETURN_PLACE.into(), ctxt).unwrap() ==	1	1	1	1	1	1	1	1	1	1	0	0	0	0	0	1	1	1	1	1	1	1	1	1	1	1	1	1
not yet implemented: cast kind PointerWithExposedProvenance	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1
not yet implemented: cast kind FloatToInt	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1
PCG Assertion Failed : [main::set] capabilities.get(RETURN_PLACE.into(), ctxt).unwrap() ==	1	1	1	1	1	1	1	1	1	1	0	0	0	0	0	1	1	1	1	1	1	1	1	1	1	1	1	1
not yet implemented: cast kind IntToFloat	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	1	1	1	1	1	1	1	1	1	1
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 }	0	0	0	1	1	1	1	1	1	1	0	0	0	0	0	1	1	1	1	1	1	1	1	1	1	1	1	1
Box<dyn Any>	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1
expected structlike or enumlike type	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1
called `Result::unwrap()` on an `Err` value: DependencyError([("wand encoder", "WandEncTask { data: FunctionData { def_id: DefId(2:11056 ~ core[b6b5]::result::{impl#0}::as_ref), substs: [std::string::String, &'?59 str], caller_def_id: Some(DefId(0:3 ~ core_result_doctest_593[84c6]::main)) } }", []), ("wand encoder", "Unsupported(\"coupled edges: CoupleInputError\")", [])])	1	1	1	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
unsupported: constant scalars that are not primitives	604	605	666	697	699	747	747	713	715	749	693	693	547	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
bug: lifetime-annotated structs	263	299	314	319	375	0	0	204	205	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
bug: indexing during parametric const encoding	191	151	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
unsupported: enum types in indirect predicate encoder	0	0	0	0	0	0	0	0	0	0	1028	1028	980	1655	1655	0	0	0	0	0	0	0	0	0	0	0	0	0
unsupported: indirect constant values	14	14	16	16	16	16	16	16	16	16	16	16	15	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
bug: region index out-of-bounds	51	51	60	61	0	0	0	0	0	0	0	0	0	0	0	1	1	1	1	1	1	1	1	1	0	0	0	0
offending pos id is missing for error VerificationError { full_id: "invariant.not.established:insufficient.permission", pos_id: None, offending_pos_id: None, reason_pos_id: None, message: "Loop invariant acc(p_Ref_immutable(_1p, s_Slice_type(s_UInt_u8_type())), write) might not hold on entry. There might be insufficient permission to access p_Ref_immutable(_1p, s_Slice_type(s_UInt_u8_type())) (<no position>)\n", counterexample: None }	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	1
unsupported: trait objects	100	101	101	101	101	101	101	101	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
unsupported: function shapes containing alias types (pcg)	221	149	150	175	175	255	255	205	211	261	197	197	452	452	452	0	0	0	0	0	0	0	0	0	0	0	0	0
assertion `left == right` failed	2	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
bug: const ptr offset overflow	60	60	70	73	73	164	164	142	148	170	98	98	80	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
unsupported: recursive struct types	138	138	138	138	138	138	138	138	138	138	138	138	132	132	132	108	108	108	109	109	0	0	0	0	0	0	0	0
unsupported: constant pointer-to-pointers	65	65	66	70	70	139	139	114	123	148	80	80	60	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
bug: g_params uses concrete substs instead of identity args	98	98	109	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
index out of bounds: the len is 0 but the index is 0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	2
unsupported: function shapes with incomparable regions (pcg)	4	4	4	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
index out of bounds: the len is 1 but the index is 1	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	4
unsupported: invalid uninitialized bytes in constants	83	83	91	92	92	100	100	96	97	101	86	86	76	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0

Prusti Analysis — Databases

Category comparison