Skip to content

Commit 834bda4

Browse files
author
Carolyn Zech
committed
resolve TODO
1 parent ddaeb9b commit 834bda4

2 files changed

Lines changed: 2 additions & 5 deletions

File tree

scripts/autoharness_analyzer/README.md

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,5 +14,3 @@ on the standard library. The scanner_results/ directory contains the CSV files t
1414
The output is `autoharness_data.md`, which contains Markdown tables summarizing the autoharness application across all the crates in the standard library.
1515

1616
One of the tables has a column for "Skipped Type Categories." Generally speaking, "precise types" are what we think of as actual Rust types, and "type categories" are my subjective sense of how to group those types further. For example, `&mut i32` and `&mut u32` are two precise types, but they're in the same type category `&mut`. See the code for exact details on how we create type categories; the TL;DR is that we have a few hardcoded ones for raw pointers and references, and the rest we create using a fully-qualified path splitting heuristic.
17-
18-
See TODOs for known limitations and future work.

scripts/autoharness_analyzer/src/make_tables.rs

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,8 @@ fn chosen_overview_table(
3030
safe_count += 1;
3131
}
3232
} else {
33-
// TODO: Note that we don't include these functions in the totals, so the metrics are still right,
34-
// and thankfully it seems to affect a pretty small slice of the whole.
35-
// (The todo is for Carolyn to investigate these mistakes).
33+
// See https://github.com/model-checking/verify-rust-std/pull/350#discussion_r2091698600
34+
// for examples of when such discrepancies appear
3635
println!(
3736
"[WARNING] Function {} is in in autoharness metadata but absent in scanner tool output",
3837
fn_name

0 commit comments

Comments
 (0)