From 5112837a5c1e55c8a1e7be6e7a5a81cad082103d Mon Sep 17 00:00:00 2001 From: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com> Date: Sun, 5 Jul 2026 01:38:36 +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 45c6de17001d6..c8b6b64944f15 100644 --- a/scripts/kani-std-analysis/metrics-data-core.json +++ b/scripts/kani-std-analysis/metrics-data-core.json @@ -1238,6 +1238,28 @@ "verified_safe_fns_under_contract": 112, "verified_safe_fns_with_loop_under_contract": 1, "total_functions_under_contract_all_crates": 424 + }, + { + "date": "2026-07-05", + "total_unsafe_fns": 7166, + "total_unsafe_fns_with_loop": 22, + "total_safe_abstractions": 1899, + "total_safe_abstractions_with_loop": 90, + "total_safe_fns": 16120, + "total_safe_fns_with_loop": 783, + "unsafe_fns_under_contract": 290, + "unsafe_fns_with_loop_under_contract": 3, + "verified_unsafe_fns_under_contract": 254, + "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": 115, + "safe_fns_with_loop_under_contract": 1, + "verified_safe_fns_under_contract": 112, + "verified_safe_fns_with_loop_under_contract": 1, + "total_functions_under_contract_all_crates": 424 } ] } \ 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 63242486db857..2cea5fa31cd3e 100644 --- a/scripts/kani-std-analysis/metrics-data-std.json +++ b/scripts/kani-std-analysis/metrics-data-std.json @@ -1121,6 +1121,28 @@ "verified_safe_fns_under_contract": 0, "verified_safe_fns_with_loop_under_contract": 0, "total_functions_under_contract_all_crates": 424 + }, + { + "date": "2026-07-05", + "total_unsafe_fns": 183, + "total_unsafe_fns_with_loop": 12, + "total_safe_abstractions": 517, + "total_safe_abstractions_with_loop": 44, + "total_safe_fns": 4133, + "total_safe_fns_with_loop": 186, + "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": 424 } ] } \ No newline at end of file