From 072967378f068879de76afd7ed5a5c612f876f7b Mon Sep 17 00:00:00 2001 From: tautschnig <1144736+tautschnig@users.noreply.github.com> Date: Sun, 13 Jul 2025 02:06:47 +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 6f05a4fde4ee1..5fed8b0908d7f 100644 --- a/scripts/kani-std-analysis/metrics-data-core.json +++ b/scripts/kani-std-analysis/metrics-data-core.json @@ -402,6 +402,28 @@ "verified_safe_fns_under_contract": 111, "verified_safe_fns_with_loop_under_contract": 0, "total_functions_under_contract_all_crates": 356 + }, + { + "date": "2025-07-13", + "total_unsafe_fns": 7259, + "total_unsafe_fns_with_loop": 16, + "total_safe_abstractions": 1839, + "total_safe_abstractions_with_loop": 74, + "total_safe_fns": 15872, + "total_safe_fns_with_loop": 739, + "unsafe_fns_under_contract": 228, + "unsafe_fns_with_loop_under_contract": 2, + "verified_unsafe_fns_under_contract": 219, + "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": 113, + "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": 356 } ] } \ 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 3f69a34a76520..fc8966b0169be 100644 --- a/scripts/kani-std-analysis/metrics-data-std.json +++ b/scripts/kani-std-analysis/metrics-data-std.json @@ -285,6 +285,28 @@ "verified_safe_fns_under_contract": 0, "verified_safe_fns_with_loop_under_contract": 0, "total_functions_under_contract_all_crates": 356 + }, + { + "date": "2025-07-13", + "total_unsafe_fns": 182, + "total_unsafe_fns_with_loop": 12, + "total_safe_abstractions": 490, + "total_safe_abstractions_with_loop": 46, + "total_safe_fns": 4125, + "total_safe_fns_with_loop": 189, + "unsafe_fns_under_contract": 9, + "unsafe_fns_with_loop_under_contract": 0, + "verified_unsafe_fns_under_contract": 2, + "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": 356 } ] } \ No newline at end of file