From 27931efa509625e81c2afaaa5df2bf17e59757fc Mon Sep 17 00:00:00 2001 From: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com> Date: Sun, 24 Aug 2025 01:13:49 +0000 Subject: [PATCH] Update Kani metrics --- .../kani-std-analysis/metrics-data-core.json | 22 +++++++++++++++++++ .../kani-std-analysis/metrics-data-std.json | 22 +++++++++++++++++++ 2 files changed, 44 insertions(+) diff --git a/scripts/kani-std-analysis/metrics-data-core.json b/scripts/kani-std-analysis/metrics-data-core.json index 058429283a32b..2717dc95af26d 100644 --- a/scripts/kani-std-analysis/metrics-data-core.json +++ b/scripts/kani-std-analysis/metrics-data-core.json @@ -600,6 +600,28 @@ "verified_safe_fns_under_contract": 111, "verified_safe_fns_with_loop_under_contract": 0, "total_functions_under_contract_all_crates": 417 + }, + { + "date": "2025-08-24", + "total_unsafe_fns": 7194, + "total_unsafe_fns_with_loop": 22, + "total_safe_abstractions": 1886, + "total_safe_abstractions_with_loop": 88, + "total_safe_fns": 15820, + "total_safe_fns_with_loop": 750, + "unsafe_fns_under_contract": 284, + "unsafe_fns_with_loop_under_contract": 3, + "verified_unsafe_fns_under_contract": 253, + "verified_unsafe_fns_with_loop_under_contract": 1, + "safe_abstractions_under_contract": 77, + "safe_abstractions_with_loop_under_contract": 0, + "verified_safe_abstractions_under_contract": 77, + "verified_safe_abstractions_with_loop_under_contract": 0, + "safe_fns_under_contract": 114, + "safe_fns_with_loop_under_contract": 0, + "verified_safe_fns_under_contract": 111, + "verified_safe_fns_with_loop_under_contract": 0, + "total_functions_under_contract_all_crates": 417 } ] } \ No newline at end of file diff --git a/scripts/kani-std-analysis/metrics-data-std.json b/scripts/kani-std-analysis/metrics-data-std.json index 64c44ea9cc705..4f9240cfab549 100644 --- a/scripts/kani-std-analysis/metrics-data-std.json +++ b/scripts/kani-std-analysis/metrics-data-std.json @@ -483,6 +483,28 @@ "verified_safe_fns_under_contract": 0, "verified_safe_fns_with_loop_under_contract": 0, "total_functions_under_contract_all_crates": 417 + }, + { + "date": "2025-08-24", + "total_unsafe_fns": 184, + "total_unsafe_fns_with_loop": 12, + "total_safe_abstractions": 505, + "total_safe_abstractions_with_loop": 47, + "total_safe_fns": 4181, + "total_safe_fns_with_loop": 190, + "unsafe_fns_under_contract": 10, + "unsafe_fns_with_loop_under_contract": 1, + "verified_unsafe_fns_under_contract": 7, + "verified_unsafe_fns_with_loop_under_contract": 0, + "safe_abstractions_under_contract": 0, + "safe_abstractions_with_loop_under_contract": 0, + "verified_safe_abstractions_under_contract": 0, + "verified_safe_abstractions_with_loop_under_contract": 0, + "safe_fns_under_contract": 0, + "safe_fns_with_loop_under_contract": 0, + "verified_safe_fns_under_contract": 0, + "verified_safe_fns_with_loop_under_contract": 0, + "total_functions_under_contract_all_crates": 417 } ] } \ No newline at end of file