Skip to content

Include alloc in the Kani metrics collected by run-kani.sh - #697

Merged
feliperodri merged 1 commit into
model-checking:mainfrom
Tianshu-Huang:run-kani-include-alloc
Sep 25, 2026
Merged

feliperodri merged 1 commit into
model-checking:mainfrom
Tianshu-Huang:run-kani-include-alloc

Conversation

@Tianshu-Huang

Copy link
Copy Markdown

run-kani.sh --run metrics computes contract metrics for core and std only; alloc is one of the three crates the autoharness baseline is measured on, so adding it in this PR.

std-analysis.sh already produces alloc_scan_*.csv. The only other piece is the seed metrics-data-alloc.json, which kani_std_analysis.py needs to exist before it can append the first entry.

Note that until #696 lands, alloc's *_under_contract numbers will read 0 for the same reason core's and std's currently do.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@Tianshu-Huang
Tianshu-Huang requested a review from a team as a code owner September 24, 2026 22:33
@feliperodri feliperodri added the Maintenance Maintenance related issues for the challange label Sep 25, 2026
@feliperodri
feliperodri added this pull request to the merge queue Sep 25, 2026
Merged via the queue into model-checking:main with commit 29a6bf7 Sep 25, 2026
30 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Maintenance Maintenance related issues for the challange

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants