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

Allow modifies clause for verification only #3098

Merged
merged 12 commits into from
Apr 2, 2024
Merged

Allow modifies clause for verification only #3098

merged 12 commits into from
Apr 2, 2024

Commits on Mar 28, 2024

  1. Allow modifies clause for verification only 

    Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    609619a View commit details
    Browse the repository at this point in the history

  2. Add recursion attribute 

    Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    2c0a909 View commit details
    Browse the repository at this point in the history

  3. Remove check_is_contract_safe function 

    Contracts now are able to reason about the heap, thus,
this safety check is no longer necessary.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    0c9a0fa View commit details
    Browse the repository at this point in the history

  4. Replace attribute for any_modifies 

    Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    8c4eb46 View commit details
    Browse the repository at this point in the history

Commits on Mar 29, 2024

  1. Remove unused functions and imports 

    Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Mar 29, 2024
    Configuration menu
    Copy the full SHA
    e8186e7 View commit details
    Browse the repository at this point in the history

  2. Update regression tests after removing check_is_contract_safe 

    Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Mar 29, 2024
    Configuration menu
    Copy the full SHA
    cd99121 View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2024

  1. Include documentation for recursion attribute 

    Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    463cee9 View commit details
    Browse the repository at this point in the history

  2. Add missing newline 

    Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    39f68ba View commit details
    Browse the repository at this point in the history

  3. Clarify condition for any_modifies transformation 

    Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    3d37518 View commit details
    Browse the repository at this point in the history

  4. Use diagnose info instead of name in reachability 

    Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    9c43563 View commit details
    Browse the repository at this point in the history

  5. Kani fails without proper annotation for recursive functions 

    Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
    @feliperodri
    feliperodri committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    6635a93 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'main' into only-verify-contracts

    @feliperodri
    feliperodri authored Apr 2, 2024
    Configuration menu
    Copy the full SHA
    b9615bf View commit details
    Browse the repository at this point in the history