Skip to content

Conversation

celinval
Copy link
Contributor

  • Contracts cannot duplicate some attributes. I think we need a better solution than just duplicate all attributes, but for now just filter the ones we know are problematic.
  • Do not make contract generated functions const when annotating constant functions.
  • I also moved the compilation of no_core up since it is much faster.

Call-out

Need to add a test.

Resolves #3251
Resolves #3254

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

  - Contracts cannot duplicate some attributes. I think we need a better
    solution than just duplicate all attributes, but for now just filter
    the ones we know are problematic.
  - Do not make contract generated functions `const` when annotating
    constant functions.
  - I also moved the compilation of no_core up since it is much faster.
@celinval celinval requested a review from a team as a code owner June 11, 2024 16:15
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jun 11, 2024
 - The `std` crate has type dylib and rlib.
@celinval celinval force-pushed the issue-3251-core-contract branch from 340a337 to 9ae71b6 Compare June 11, 2024 18:22
Copy link
Contributor

@jaisnan jaisnan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm approving this. I assume there might some other attributes that might cause issues, but we can always add more to the filter or improve the filter in any case.

@celinval celinval enabled auto-merge (squash) June 11, 2024 18:36
@celinval
Copy link
Contributor Author

I think unstable might be one... not sure yet.

@celinval celinval merged commit ca110f7 into model-checking:main Jun 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Cannot verify a constant function with contracts Kani contract cannot be applied to functions with rustc_diagnostic_item
2 participants