Skip to content

Derive Arbitrary for various core_arch::x86 types #348

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

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from

Conversation

tautschnig
Copy link
Member

This enables autoharness to generate an additional 4067 harnesses (and successfully prove 363 of them).

Using a patch instead of directly modifying the source code here for library/stdarch is a git submodule. Modifying the source code directly would require forking that other repository, tweaking our submodule pointer, and thereby causing additional challenges for our fork update automation.

The long-term solution should be automated derive-arbitrary support in autoharness.

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

This enables autoharness to generate an additional 4067 harnesses (and
successfully prove 363 of them).

Using a patch instead of directly modifying the source code here for
`library/stdarch` is a git submodule. Modifying the source code directly
would require forking that other repository, tweaking our submodule
pointer, and thereby causing additional challenges for our fork update
automation.

The long-term solution should be automated derive-arbitrary support in
autoharness.
@tautschnig tautschnig requested a review from a team as a code owner April 30, 2025 10:39
@tautschnig tautschnig marked this pull request as draft April 30, 2025 11:18
@tautschnig
Copy link
Member Author

Requires updating to a more recent Kani version to have the SIMD fix included.

@tautschnig tautschnig self-assigned this Apr 30, 2025
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