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.

Sign up for GitHub

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

Jump to bottom

Cleanup work due to enabling standard library verification #3257

Open
2 of 5 tasks
celinval opened this issue Jun 11, 2024 · 0 comments
Open
2 of 5 tasks

Cleanup work due to enabling standard library verification #3257

celinval opened this issue Jun 11, 2024 · 0 comments
Assignees
@celinval @jaisnan
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected. [I] Refactoring / Clean Up Refactoring or cleaning up of existing code

Comments

@celinval
Copy link
Contributor

celinval commented Jun 11, 2024 •
edited
Loading

Keeping a list of things that we need to improve to make the code more maintainable and less fragile:

  • Unify kani and kani_core logic. Add intrinsics and Arbitrary support for no_core #3230 introduced duplicated logic.
  • Improve contract attribute handling.
  • Safe handling rustc ast lowering in cases where they add extra generic argument.
    • One issue we bumped into is with constant functions and feature effect enabled.
  • Rename unstable function and re-add them to the kani_core::mem functions.
  • Enable any_array for the standard library.
@celinval celinval added [I] Refactoring / Clean Up Refactoring or cleaning up of existing code [C] Internal Tracks some internal work. I.e.: Users should not be affected. labels Jun 11, 2024
@celinval celinval mentioned this issue Jun 21, 2024
Merged
@jaisnan jaisnan mentioned this issue Jul 9, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Aug 6, 2024
@jaisnan
Unify kani library and kani core logic (#3333)
2a0e9bd 
1. Unifies `Kani library` and `kani_core` for `Arbitrary`, `mem` and
`intrinsics` along with the `internal` module.
2. Adjusts some regression expected files to reflect the new underlying
source of Arbitrary

Related to ##3257

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@celinval celinval

@jaisnan jaisnan

Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected. [I] Refactoring / Clean Up Refactoring or cleaning up of existing code
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@celinval @jaisnan