tautschnig · github-actions · Feb 24, 2025 · Feb 25, 2025 · Feb 25, 2025 · Feb 25, 2025
diff --git a/doc/mdbook-metrics/src/main.rs b/doc/mdbook-metrics/src/main.rs
@@ -44,6 +44,25 @@ fn run_kani_metrics_script() -> Result<(), Error> {
     Command::new("python")
         .args(&[
             "kani_std_analysis.py",
+            "--crate",
+            "core",
+            "--metrics-file",
+            "metrics-data-core.json",
+            "--plot-only",
+            "--plot-dir",
+            &tools_path.to_string_lossy(),
+        ])
+        .stdout(std::process::Stdio::null())
+        .stderr(std::process::Stdio::null())
+        .status()?;
+
+    Command::new("python")
+        .args(&[
+            "kani_std_analysis.py",
+            "--crate",
+            "std",
+            "--metrics-file",
+            "metrics-data-std.json",
             "--plot-only",
             "--plot-dir",
             &tools_path.to_string_lossy(),
@@ -83,12 +102,19 @@ fn add_graphs(chapter: &mut Chapter) {
 
 Note that these metrics are for x86-64 architectures.
 
-## `core`
+### `core`
 ![Unsafe Metrics](core_unsafe_metrics.png)
 
 ![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
 
 ![Safe Metrics](core_safe_metrics.png)
+
+### `std`
+![Unsafe Metrics](std_unsafe_metrics.png)
+
+![Safe Abstractions Metrics](std_safe_abstractions_metrics.png)
+
+![Safe Metrics](std_safe_metrics.png)
 "#;
 
     chapter.content.push_str(new_content);

diff --git a/library/backtrace b/library/backtrace
diff --git a/library/stdarch b/library/stdarch
diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
diff --git a/scripts/kani-std-analysis/metrics-data.json → .../kani-std-analysis/metrics-data-core.json b/scripts/kani-std-analysis/metrics-data.json → .../kani-std-analysis/metrics-data-core.json
@@ -116,6 +116,28 @@
       "safe_fns_under_contract": 77,
       "verified_safe_fns_under_contract": 75,
       "total_functions_under_contract": 273
+    },
+    {
+      "date": "2025-03-23",
+      "total_unsafe_fns": 7215,
+      "total_unsafe_fns_with_loop": 14,
+      "total_safe_abstractions": 1792,
+      "total_safe_abstractions_with_loop": 71,
+      "total_safe_fns": 15383,
+      "total_safe_fns_with_loop": 735,
+      "unsafe_fns_under_contract": 190,
+      "unsafe_fns_with_loop_under_contract": 1,
+      "verified_unsafe_fns_under_contract": 132,
+      "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": 271
     }
   ]
 }
diff --git a/scripts/kani-std-analysis/metrics-data-std.json b/scripts/kani-std-analysis/metrics-data-std.json
@@ -0,0 +1,26 @@
+{
+  "results": [
+    {
+      "date": "2025-03-23",
+      "total_unsafe_fns": 179,
+      "total_unsafe_fns_with_loop": 12,
+      "total_safe_abstractions": 567,
+      "total_safe_abstractions_with_loop": 43,
+      "total_safe_fns": 4087,
+      "total_safe_fns_with_loop": 175,
+      "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": 271
+    }
+  ]
+}
diff --git a/scripts/kani-std-analysis/std-analysis.sh b/scripts/kani-std-analysis/std-analysis.sh
@@ -65,7 +65,6 @@ then
 fi
 cargo new std_lib_analysis --lib
 cd std_lib_analysis
-sed -i '1i cargo-features = ["edition2024"]' Cargo.toml
 
 echo '
 pub fn dummy() {

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
@@ -309,7 +309,12 @@ main() {
         ./std-analysis.sh $build_dir
         pip install -r requirements.txt
         echo "Computing Kani-specific metrics..."
-        ./kani_std_analysis.py --kani-list-file $current_dir/kani-list.json
+        ./kani_std_analysis.py --crate core \
+          --kani-list-file $current_dir/kani-list.json \
+          --metrics-file metrics-data-core.json
+        ./kani_std_analysis.py --crate std \
+          --kani-list-file $current_dir/kani-list.json \
+          --metrics-file metrics-data-std.json
         popd
         rm kani-list.json
     fi
+1 −1		.github/workflows/main.yml
+1 −1		Cargo.toml
+10 −1		src/backtrace/dbghelp32.rs
+20 −20		src/backtrace/dbghelp64.rs
+20 −27		src/backtrace/libunwind.rs
+5 −10		src/backtrace/miri.rs
+7 −7		src/backtrace/mod.rs
+1 −4		src/backtrace/noop.rs
+2 −0		src/dbghelp.rs
+2 −2		src/print/fuchsia.rs
+89 −116		src/symbolize/dbghelp.rs
+46 −53		src/symbolize/gimli.rs
+13 −8		src/symbolize/gimli/elf.rs
+6 −13		src/symbolize/gimli/libs_aix.rs
+1 −1		src/symbolize/gimli/libs_illumos.rs
+1 −1		src/symbolize/gimli/libs_libnx.rs
+15 −18		src/symbolize/gimli/libs_windows.rs
+8 −10		src/symbolize/gimli/mmap_unix.rs
+27 −29		src/symbolize/gimli/mmap_windows.rs
+3 −3		src/symbolize/gimli/xcoff.rs
+2 −2		src/symbolize/mod.rs
+0 −4		src/windows_sys.rs
+0 −53		src/windows_sys_arm32_shim.rs