From 8e4313b790eff754b06b9acf5478b9f5512c79e1 Mon Sep 17 00:00:00 2001 From: tautschnig <1144736+tautschnig@users.noreply.github.com> Date: Sun, 4 May 2025 01:26:37 +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 6ff679b792f60..f2dc6b781b340 100644 --- a/scripts/kani-std-analysis/metrics-data-core.json +++ b/scripts/kani-std-analysis/metrics-data-core.json @@ -226,6 +226,28 @@ "verified_safe_fns_under_contract": 75, "verified_safe_fns_with_loop_under_contract": 0, "total_functions_under_contract_all_crates": 274 + }, + { + "date": "2025-05-04", + "total_unsafe_fns": 7249, + "total_unsafe_fns_with_loop": 16, + "total_safe_abstractions": 1813, + "total_safe_abstractions_with_loop": 74, + "total_safe_fns": 15737, + "total_safe_fns_with_loop": 744, + "unsafe_fns_under_contract": 193, + "unsafe_fns_with_loop_under_contract": 1, + "verified_unsafe_fns_under_contract": 135, + "verified_unsafe_fns_with_loop_under_contract": 0, + "safe_abstractions_under_contract": 41, + "safe_abstractions_with_loop_under_contract": 0, + "verified_safe_abstractions_under_contract": 41, + "verified_safe_abstractions_with_loop_under_contract": 0, + "safe_fns_under_contract": 77, + "safe_fns_with_loop_under_contract": 0, + "verified_safe_fns_under_contract": 75, + "verified_safe_fns_with_loop_under_contract": 0, + "total_functions_under_contract_all_crates": 274 } ] } \ 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 68a3960911e01..02b1ca24e3ac6 100644 --- a/scripts/kani-std-analysis/metrics-data-std.json +++ b/scripts/kani-std-analysis/metrics-data-std.json @@ -109,6 +109,28 @@ "verified_safe_fns_under_contract": 0, "verified_safe_fns_with_loop_under_contract": 0, "total_functions_under_contract_all_crates": 274 + }, + { + "date": "2025-05-04", + "total_unsafe_fns": 179, + "total_unsafe_fns_with_loop": 12, + "total_safe_abstractions": 509, + "total_safe_abstractions_with_loop": 44, + "total_safe_fns": 4095, + "total_safe_fns_with_loop": 176, + "unsafe_fns_under_contract": 0, + "unsafe_fns_with_loop_under_contract": 0, + "verified_unsafe_fns_under_contract": 0, + "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": 274 } ] } \ No newline at end of file