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

Contracts for a few core functions #3107

Merged
merged 15 commits into from
May 29, 2024
Merged

Contracts for a few core functions #3107

merged 15 commits into from
May 29, 2024

Commits on Mar 28, 2024

  1. Add initial tests for NonNull and mem predicates

    @celinval
    celinval committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    19a4769 View commit details
    Browse the repository at this point in the history

  2. Improve library and change std tests to use crates. 

    This will allow us to re-use contracts between modules.
We still cannot compile our contracts due to
model-checking#2997
    @celinval
    celinval committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    a9c5f62 View commit details
    Browse the repository at this point in the history

  3. Add support to write_bytes used in MaybeUninit 

    Create a value of `[val; size_of::<T>()]` and check if it is a valid
combination of bytes for T.
    @celinval
    celinval committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    9a1dccf View commit details
    Browse the repository at this point in the history

  4. Add contract for replace

    @celinval
    celinval committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    86edd76 View commit details
    Browse the repository at this point in the history

  5. Add missing Cargo.toml

    @celinval
    celinval committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    c38136f View commit details
    Browse the repository at this point in the history

Commits on May 11, 2024

  1. Merge remote-tracking branch 'origin/main' into std-non-null

    @celinval
    celinval committed May 11, 2024
    Configuration menu
    Copy the full SHA
    3c74b6c View commit details
    Browse the repository at this point in the history

Commits on May 13, 2024

  1. Rename a few things

    @celinval
    celinval committed May 13, 2024
    Configuration menu
    Copy the full SHA
    3dffab5 View commit details
    Browse the repository at this point in the history

Commits on May 14, 2024

  1. Add a new intrinsic to check value validity

    @celinval
    celinval committed May 14, 2024
    Configuration menu
    Copy the full SHA
    e844934 View commit details
    Browse the repository at this point in the history

  2. Finish polishing contracts and create expected

    @celinval
    celinval committed May 14, 2024
    Configuration menu
    Copy the full SHA
    7469d61 View commit details
    Browse the repository at this point in the history

  3. revert space changes

    @celinval
    celinval committed May 14, 2024
    Configuration menu
    Copy the full SHA
    e2b4a20 View commit details
    Browse the repository at this point in the history

  4. Clean up changes

    @celinval
    celinval committed May 14, 2024
    Configuration menu
    Copy the full SHA
    122e3a8 View commit details
    Browse the repository at this point in the history

Commits on May 24, 2024

  1. Address comments and fix issue in invalid values 

    - I noticed that invalid values should be checked for
  copy_nonoverlapping statement. I added an unsupported check for now
  so we can actually implement the check later.
    @celinval
    celinval committed May 24, 2024
    Configuration menu
    Copy the full SHA
    5f4a69b View commit details
    Browse the repository at this point in the history

Commits on May 28, 2024

  1. Fix regression

    @celinval
    celinval committed May 28, 2024
    Configuration menu
    Copy the full SHA
    c18754d View commit details
    Browse the repository at this point in the history

Commits on May 29, 2024

  1. Update kani-compiler/src/kani_middle/transform/body.rs

    @celinval
    celinval authored May 29, 2024
    Configuration menu
    Copy the full SHA
    2a8cfdb View commit details
    Browse the repository at this point in the history

  2. Merge branch 'main' into std-non-null

    @celinval
    celinval authored May 29, 2024
    Configuration menu
    Copy the full SHA
    d295ce3 View commit details
    Browse the repository at this point in the history