Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Don't translate provided methods that we don't use #540

Merged
merged 8 commits into from
Jan 30, 2025

Conversation

Nadrieril
Copy link
Member

This reduces the size of charon's output by giving a new meaning to opacity on traits/impls: now, an opaque trait/impl will not have its provided methods (those with a default body) translated, unless they are used. This removes significant churn when translating the Iterator trait, among others.

This behavior can be turned off with the --translate-all-methods flag.

@Nadrieril Nadrieril force-pushed the lazy-translate-methods branch from 91756fe to 9d7c40a Compare January 30, 2025 12:52
@Nadrieril Nadrieril force-pushed the lazy-translate-methods branch 2 times, most recently from 0ba4770 to d3c9ee1 Compare January 30, 2025 14:15
@Nadrieril Nadrieril force-pushed the lazy-translate-methods branch from d3c9ee1 to ab69275 Compare January 30, 2025 14:30
@Nadrieril Nadrieril merged commit 30cab88 into AeneasVerif:main Jan 30, 2025
3 of 5 checks passed
@Nadrieril Nadrieril deleted the lazy-translate-methods branch January 30, 2025 15:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant