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

Add a few intrinsics contracts #37

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

Add a few intrinsics contracts #37

wants to merge 8 commits into from

Commits on Jul 23, 2024

  1. Add a few intrinsics contracts 

    - This is not working due to a Kani limitation
    @celinval
    celinval committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    aa1b9c2 View commit details
    Browse the repository at this point in the history

  2. Fix copy* contract to make it untyped 

    The intrinsics `copy` and `copy_nonoverlapping` are untyped copies,
so they don't respect the validity requirements of `T`.
    @celinval
    celinval committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    1ad91c8 View commit details
    Browse the repository at this point in the history

  3. Fix Rust build and make MetadataPredicates public

    @celinval
    celinval committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    898f08f View commit details
    Browse the repository at this point in the history

  4. Add a few ensure clauses

    @celinval
    celinval committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    79c6536 View commit details
    Browse the repository at this point in the history

Commits on Sep 18, 2024

  1. Merge remote-tracking branch 'origin/main' into verify-intrinsics 

    # Conflicts:
#	library/core/src/intrinsics.rs
    @celinval
    celinval committed Sep 18, 2024
    Configuration menu
    Copy the full SHA
    0182ea1 View commit details
    Browse the repository at this point in the history

Commits on Sep 19, 2024

  1. Final adjustments for new harnesses

    @celinval
    celinval committed Sep 19, 2024
    Configuration menu
    Copy the full SHA
    87dc890 View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2024

  1. Clean up arbitrary pointer

    @celinval
    celinval committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    a38c161 View commit details
    Browse the repository at this point in the history

  2. Update intrinsics.rs 

    Silly brain... 🤦‍♀️
    @celinval
    celinval committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    d41e5c1 View commit details
    Browse the repository at this point in the history