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

Define a struct-level #[safety_constraint(...)] attribute #3270

Merged
merged 49 commits into from
Jul 31, 2024
Merged

Define a struct-level #[safety_constraint(...)] attribute #3270

merged 49 commits into from
Jul 31, 2024

Commits on Jul 23, 2024

  1. Add expected & ui tests

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    51b7b2f View commit details
    Browse the repository at this point in the history

  2. Another newline

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    441c26e View commit details
    Browse the repository at this point in the history

  3. Use references for expressions (Invariant needs fix)

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    f043724 View commit details
    Browse the repository at this point in the history

  4. Apply fixes for format

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    8f0ca5b View commit details
    Browse the repository at this point in the history

  5. Some refactoring and documentation

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    accec8e View commit details
    Browse the repository at this point in the history

  6. Fix bug and all tests

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    f89ae0f View commit details
    Browse the repository at this point in the history

  7. Add new test for Arbitrary-only invariant behavior

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    7d7f294 View commit details
    Browse the repository at this point in the history

  8. Add test with functions

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    09e3ee5 View commit details
    Browse the repository at this point in the history

  9. Add test where invariant is violated thru mut

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    472e659 View commit details
    Browse the repository at this point in the history

  10. Add support for kani::invariant attribute

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    9c92e7b View commit details
    Browse the repository at this point in the history

  11. Add positive test for kani::invariant impl

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    bb70242 View commit details
    Browse the repository at this point in the history

  12. Declare proc_macro_error

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    b7cd512 View commit details
    Browse the repository at this point in the history

  13. Add two UI tests

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    b3cc69a View commit details
    Browse the repository at this point in the history

  14. Fix comments in all test cases

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    35b41fc View commit details
    Browse the repository at this point in the history

  15. Fix format

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    7bc5c3a View commit details
    Browse the repository at this point in the history

  16. Move macro to lib.rs, fix tests

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    ba59f8f View commit details
    Browse the repository at this point in the history

  17. Fix invalid-pred-error test.

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    ad55213 View commit details
    Browse the repository at this point in the history

  18. Fix another test

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    aa935fe View commit details
    Browse the repository at this point in the history

  19. Add double-attr-invariant test

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    631b103 View commit details
    Browse the repository at this point in the history

  20. Derive Arbitrary as well, fix tests

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    f2ee78c View commit details
    Browse the repository at this point in the history

  21. Add another test

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    e3ebe57 View commit details
    Browse the repository at this point in the history

  22. Restore import

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    d0ae3bd View commit details
    Browse the repository at this point in the history

  23. Remove renamed test cases

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    92fcede View commit details
    Browse the repository at this point in the history

  24. Add is_safe calls to generated return value

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    1fc797e View commit details
    Browse the repository at this point in the history

  25. Merge branch 'main' into attr-invariant

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    df7f002 View commit details
    Browse the repository at this point in the history

  26. Fix fmt

    @adpaco-aws
    adpaco-aws committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    64a5a8b View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2024

  1. Tweak generation of Invariant to work with both attr types

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    812a2b0 View commit details
    Browse the repository at this point in the history

  2. Remove code related to outdated attribute

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    5078b07 View commit details
    Browse the repository at this point in the history

  3. Refactor safe body generation

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    b05de12 View commit details
    Browse the repository at this point in the history

  4. Fix default safe body for unnamed fields

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    7cc466f View commit details
    Browse the repository at this point in the history

  5. Fix attribute tests (still need to be moved)

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    dddc556 View commit details
    Browse the repository at this point in the history

  6. Fix generation for Arbitrary and refactor

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    64010a9 View commit details
    Browse the repository at this point in the history

  7. Pass down trait name for better errors

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    74c338e View commit details
    Browse the repository at this point in the history

  8. Add some documentation

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    3d19c34 View commit details
    Browse the repository at this point in the history

  9. Fix UI tests mostly

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    a2ed3db View commit details
    Browse the repository at this point in the history

  10. Fix double-attr test

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    24a7a9c View commit details
    Browse the repository at this point in the history

  11. Merge branch 'main' into attr-invariant

    @adpaco-aws
    adpaco-aws committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    0ed1f23 View commit details
    Browse the repository at this point in the history

Commits on Jul 29, 2024

  1. More error handling, improve UI testing

    @adpaco-aws
    adpaco-aws committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    180105c View commit details
    Browse the repository at this point in the history

  2. Add more tests and do some renames

    @adpaco-aws
    adpaco-aws committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    d51fed0 View commit details
    Browse the repository at this point in the history

  3. Fixes for tests

    @adpaco-aws
    adpaco-aws committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    c909522 View commit details
    Browse the repository at this point in the history

  4. Undo some pub on derive functions

    @adpaco-aws
    adpaco-aws committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    728af85 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'main' into attr-invariant

    @adpaco-aws
    adpaco-aws committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    c1c3cf5 View commit details
    Browse the repository at this point in the history

  6. Ignore check numbers in test

    @adpaco-aws
    adpaco-aws committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    ffd858c View commit details
    Browse the repository at this point in the history

  7. Update test comment.

    @adpaco-aws
    adpaco-aws committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    206a35c View commit details
    Browse the repository at this point in the history

Commits on Jul 30, 2024

  1. Add comment missing in previous commit

    @adpaco-aws
    adpaco-aws committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    88f7443 View commit details
    Browse the repository at this point in the history

  2. Address minor comments

    @adpaco-aws
    adpaco-aws committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    8d0cd96 View commit details
    Browse the repository at this point in the history

  3. Add test for mixed attribute use

    @adpaco-aws
    adpaco-aws committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    5847597 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'main' into attr-invariant

    @adpaco-aws
    adpaco-aws committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    ae3f70b View commit details
    Browse the repository at this point in the history

Commits on Jul 31, 2024

  1. Merge branch 'main' into attr-invariant

    @adpaco-aws
    adpaco-aws authored Jul 31, 2024
    Configuration menu
    Copy the full SHA
    8e37e6d View commit details
    Browse the repository at this point in the history