Skip to content

Commit 15b5665

Browse files
Update Kani Metrics (model-checking#419)
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <[email protected]>
1 parent a914785 commit 15b5665

File tree

2 files changed

+44
-0
lines changed

2 files changed

+44
-0
lines changed

scripts/kani-std-analysis/metrics-data-core.json

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -490,6 +490,28 @@
490490
"verified_safe_fns_under_contract": 111,
491491
"verified_safe_fns_with_loop_under_contract": 0,
492492
"total_functions_under_contract_all_crates": 378
493+
},
494+
{
495+
"date": "2025-07-20",
496+
"total_unsafe_fns": 7184,
497+
"total_unsafe_fns_with_loop": 16,
498+
"total_safe_abstractions": 1844,
499+
"total_safe_abstractions_with_loop": 74,
500+
"total_safe_fns": 15913,
501+
"total_safe_fns_with_loop": 739,
502+
"unsafe_fns_under_contract": 251,
503+
"unsafe_fns_with_loop_under_contract": 2,
504+
"verified_unsafe_fns_under_contract": 242,
505+
"verified_unsafe_fns_with_loop_under_contract": 1,
506+
"safe_abstractions_under_contract": 77,
507+
"safe_abstractions_with_loop_under_contract": 0,
508+
"verified_safe_abstractions_under_contract": 77,
509+
"verified_safe_abstractions_with_loop_under_contract": 0,
510+
"safe_fns_under_contract": 113,
511+
"safe_fns_with_loop_under_contract": 0,
512+
"verified_safe_fns_under_contract": 111,
513+
"verified_safe_fns_with_loop_under_contract": 0,
514+
"total_functions_under_contract_all_crates": 379
493515
}
494516
]
495517
}

scripts/kani-std-analysis/metrics-data-std.json

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -373,6 +373,28 @@
373373
"verified_safe_fns_under_contract": 0,
374374
"verified_safe_fns_with_loop_under_contract": 0,
375375
"total_functions_under_contract_all_crates": 378
376+
},
377+
{
378+
"date": "2025-07-20",
379+
"total_unsafe_fns": 182,
380+
"total_unsafe_fns_with_loop": 12,
381+
"total_safe_abstractions": 491,
382+
"total_safe_abstractions_with_loop": 46,
383+
"total_safe_fns": 4134,
384+
"total_safe_fns_with_loop": 189,
385+
"unsafe_fns_under_contract": 9,
386+
"unsafe_fns_with_loop_under_contract": 0,
387+
"verified_unsafe_fns_under_contract": 2,
388+
"verified_unsafe_fns_with_loop_under_contract": 0,
389+
"safe_abstractions_under_contract": 0,
390+
"safe_abstractions_with_loop_under_contract": 0,
391+
"verified_safe_abstractions_under_contract": 0,
392+
"verified_safe_abstractions_with_loop_under_contract": 0,
393+
"safe_fns_under_contract": 0,
394+
"safe_fns_with_loop_under_contract": 0,
395+
"verified_safe_fns_under_contract": 0,
396+
"verified_safe_fns_with_loop_under_contract": 0,
397+
"total_functions_under_contract_all_crates": 379
376398
}
377399
]
378400
}

0 commit comments

Comments
 (0)