From 69371604fede3267d0a95c938dc3780a68f0a1cd Mon Sep 17 00:00:00 2001
From: rafaelsamenezes <8601807+rafaelsamenezes@users.noreply.github.com>
Date: Sun, 5 Oct 2025 02:03:10 +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 54f71b40cdabb..8c43d64d2c220 100644
--- a/scripts/kani-std-analysis/metrics-data-core.json
+++ b/scripts/kani-std-analysis/metrics-data-core.json
@@ -380,6 +380,28 @@
"verified_safe_fns_under_contract": 111,
"verified_safe_fns_with_loop_under_contract": 0,
"total_functions_under_contract_all_crates": 338
+ },
+ {
+ "date": "2025-10-05",
+ "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": 210,
+ "unsafe_fns_with_loop_under_contract": 2,
+ "verified_unsafe_fns_under_contract": 201,
+ "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": 338
}
]
}
\ 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 d95e46e1c70c3..8a8360642fdc0 100644
--- a/scripts/kani-std-analysis/metrics-data-std.json
+++ b/scripts/kani-std-analysis/metrics-data-std.json
@@ -263,6 +263,28 @@
"verified_safe_fns_under_contract": 0,
"verified_safe_fns_with_loop_under_contract": 0,
"total_functions_under_contract_all_crates": 338
+ },
+ {
+ "date": "2025-10-05",
+ "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": 338
}
]
}
\ No newline at end of file