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

modifies Clauses for Function Contracts #2800

Merged
merged 80 commits into from
Feb 2, 2024
Merged

modifies Clauses for Function Contracts #2800

merged 80 commits into from
Feb 2, 2024

Commits on Sep 30, 2023

  1. WIP

    @JustusAdam
    JustusAdam committed Sep 30, 2023
    Configuration menu
    Copy the full SHA
    2e6bed3 View commit details
    Browse the repository at this point in the history

  2. Sketch for new modifies clause

    @JustusAdam
    JustusAdam committed Sep 30, 2023
    Configuration menu
    Copy the full SHA
    c772a10 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2023

  1. Add explicit lifetimes to arguments and reorder code

    @JustusAdam
    JustusAdam committed Oct 1, 2023
    Configuration menu
    Copy the full SHA
    ed2e79d View commit details
    Browse the repository at this point in the history

  2. Sketch for the internal mechanisms

    @JustusAdam
    JustusAdam committed Oct 1, 2023
    Configuration menu
    Copy the full SHA
    5a8f746 View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2023

  1. Debugging proc-macro code

    @JustusAdam
    JustusAdam committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    2759469 View commit details
    Browse the repository at this point in the history

Commits on Nov 2, 2023

  1. Fixed the assigns bug

    @JustusAdam
    JustusAdam committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    9dd55a4 View commit details
    Browse the repository at this point in the history

  2. Using lifetime decoupling for modifies

    @JustusAdam
    JustusAdam committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    ba27ab6 View commit details
    Browse the repository at this point in the history

Commits on Nov 3, 2023

  1. Fix lifetime decoupling trait

    @JustusAdam
    JustusAdam committed Nov 3, 2023
    Configuration menu
    Copy the full SHA
    bbc4e99 View commit details
    Browse the repository at this point in the history

  2. Make assigns existence optional again

    @JustusAdam
    JustusAdam committed Nov 3, 2023
    Configuration menu
    Copy the full SHA
    00157cb View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'fork/main' into new-assigns-check

    @JustusAdam
    JustusAdam committed Nov 3, 2023
    Configuration menu
    Copy the full SHA
    3db104d View commit details
    Browse the repository at this point in the history

  4. Reviving havoc protection for reentry tracker

    @JustusAdam
    JustusAdam committed Nov 3, 2023
    Configuration menu
    Copy the full SHA
    559cf81 View commit details
    Browse the repository at this point in the history

Commits on Nov 7, 2023

  1. Fixed recursion tracker havocking

    @JustusAdam
    JustusAdam committed Nov 7, 2023
    Configuration menu
    Copy the full SHA
    f6d939c View commit details
    Browse the repository at this point in the history

Commits on Nov 11, 2023

  1. Fmt

    @JustusAdam
    JustusAdam committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    187c56f View commit details
    Browse the repository at this point in the history

Commits on Nov 12, 2023

  1. Cargo fix

    @JustusAdam
    JustusAdam committed Nov 12, 2023
    Configuration menu
    Copy the full SHA
    54727e2 View commit details
    Browse the repository at this point in the history

Commits on Nov 14, 2023

  1. Fix two test cases + support impl call

    @JustusAdam
    JustusAdam committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    b7c8e63 View commit details
    Browse the repository at this point in the history

  2. Fix another test case

    @JustusAdam
    JustusAdam committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    27ebf4f View commit details
    Browse the repository at this point in the history

  3. Simple havoc

    @JustusAdam
    JustusAdam committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    d9e921c View commit details
    Browse the repository at this point in the history

Commits on Nov 19, 2023

  1. Fixing Formatting and clippy

    @JustusAdam
    JustusAdam committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    ffcdc76 View commit details
    Browse the repository at this point in the history

  2. Kani fmt

    @JustusAdam
    JustusAdam committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    b833438 View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2023

  1. Fix simlpe havoc

    @JustusAdam
    JustusAdam committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    64f7e5f View commit details
    Browse the repository at this point in the history

Commits on Nov 22, 2023

  1. Fix static exclude for recursion tracker

    @JustusAdam
    JustusAdam committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    0c3cea7 View commit details
    Browse the repository at this point in the history

  2. Some changes had accidentally been reverted

    @JustusAdam
    JustusAdam committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    4b451cf View commit details
    Browse the repository at this point in the history

  3. Formatting

    @JustusAdam
    JustusAdam committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    0b6ba1e View commit details
    Browse the repository at this point in the history

  4. Allow pointer transmutes

    @JustusAdam
    JustusAdam committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    9362624 View commit details
    Browse the repository at this point in the history

  5. turns out these need to be refs

    @JustusAdam
    JustusAdam committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    7148bac View commit details
    Browse the repository at this point in the history

  6. Gracefully handle if the contract artifact is absent

    @JustusAdam
    JustusAdam committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    ba4a73e View commit details
    Browse the repository at this point in the history

  7. Clippy ...

    @JustusAdam
    JustusAdam committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    9610a9e View commit details
    Browse the repository at this point in the history

Commits on Nov 23, 2023

  1. Ignoring this error for now

    @JustusAdam
    JustusAdam committed Nov 23, 2023
    Configuration menu
    Copy the full SHA
    03ef3ce View commit details
    Browse the repository at this point in the history

Commits on Nov 29, 2023

  1. Changing how contracts communicate

    @JustusAdam
    JustusAdam committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    7b788c7 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'fork/main' into new-assigns-check

    @JustusAdam
    JustusAdam committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    904ef0e View commit details
    Browse the repository at this point in the history

  3. Formatting

    @JustusAdam
    JustusAdam committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    981a465 View commit details
    Browse the repository at this point in the history

  4. Fix Warnings

    @JustusAdam
    JustusAdam committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    f9b4ef3 View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2023

  1. Consistent use of file paths for recursion tracker

    @JustusAdam
    JustusAdam committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    12a993d View commit details
    Browse the repository at this point in the history

  2. Simplify check function editingˆ

    @JustusAdam
    JustusAdam committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    1843442 View commit details
    Browse the repository at this point in the history

  3. Fix ordering for havoc and postconditions 

    Adds test cases to ensure the order is correct
    @JustusAdam
    JustusAdam committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    00518b0 View commit details
    Browse the repository at this point in the history

  4. Extra test cases

    @JustusAdam
    JustusAdam committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    862a5d7 View commit details
    Browse the repository at this point in the history

  5. Formatting

    @JustusAdam
    JustusAdam committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    e229ad0 View commit details
    Browse the repository at this point in the history

Commits on Dec 1, 2023

  1. Grouping test cases and adding more 

    Added field and havocking test cases
    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    9d95def View commit details
    Browse the repository at this point in the history

  2. Documentation, dead code removal and unique arguments in modifies

    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    15a596b View commit details
    Browse the repository at this point in the history

  3. Test case for unique generated argument names

    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    af780f1 View commit details
    Browse the repository at this point in the history

  4. Added missing expected files

    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    e76d0b3 View commit details
    Browse the repository at this point in the history

  5. Another missing expected file

    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    907a7f9 View commit details
    Browse the repository at this point in the history

  6. Revert some clippy changes

    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    1c71508 View commit details
    Browse the repository at this point in the history

  7. Remove not strictly necessary dep

    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    e4f3cfd View commit details
    Browse the repository at this point in the history

  8. Some basic write-sets documentation

    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    9f3d102 View commit details
    Browse the repository at this point in the history

  9. Missing formatting

    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    0573d09 View commit details
    Browse the repository at this point in the history

  10. Forgot to commit this one

    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    384c2f6 View commit details
    Browse the repository at this point in the history

  11. Typo

    @JustusAdam
    JustusAdam committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    f7578a8 View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2023

  1. Tinkering with the vector test case.

    @JustusAdam
    JustusAdam committed Dec 4, 2023
    Configuration menu
    Copy the full SHA
    1fffd53 View commit details
    Browse the repository at this point in the history

Commits on Dec 14, 2023

  1. Addressing code review

    @JustusAdam
    JustusAdam committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    34e3a1b View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

    Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
    @JustusAdam @zhassan-aws
    JustusAdam and zhassan-aws authored Dec 14, 2023
    Configuration menu
    Copy the full SHA
    f01b619 View commit details
    Browse the repository at this point in the history

  3. Addressing code review leftovers

    @JustusAdam
    JustusAdam committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    f283759 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/new-assigns-check' into new-assi… 

    …gns-check
    @JustusAdam
    JustusAdam committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    6192f3e View commit details
    Browse the repository at this point in the history

  5. Added missing expected file

    @JustusAdam
    JustusAdam committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    00bfe6e View commit details
    Browse the repository at this point in the history

Commits on Dec 15, 2023

  1. Fixed the expected file

    @JustusAdam
    JustusAdam committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    9c6b876 View commit details
    Browse the repository at this point in the history

  2. Added test cases for global variable modifications

    @JustusAdam
    JustusAdam committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    a5dfccd View commit details
    Browse the repository at this point in the history

Commits on Dec 23, 2023

  1. Apply suggestions from code review 

    Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
    @JustusAdam @feliperodri
    JustusAdam and feliperodri authored Dec 23, 2023
    Configuration menu
    Copy the full SHA
    c5b6a2b View commit details
    Browse the repository at this point in the history

  2. Suggestions from @feliperodri

    @JustusAdam
    JustusAdam committed Dec 23, 2023
    Configuration menu
    Copy the full SHA
    6892afc View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/new-assigns-check' into new-assi… 

    …gns-check
    @JustusAdam
    JustusAdam committed Dec 23, 2023
    Configuration menu
    Copy the full SHA
    0819432 View commit details
    Browse the repository at this point in the history

Commits on Dec 25, 2023

  1. Merge remote-tracking branch 'fork/main' into new-assigns-check

    @JustusAdam
    JustusAdam committed Dec 25, 2023
    Configuration menu
    Copy the full SHA
    55c5583 View commit details
    Browse the repository at this point in the history

Commits on Dec 26, 2023

  1. Update contract code to stable MIR

    @JustusAdam
    JustusAdam committed Dec 26, 2023
    Configuration menu
    Copy the full SHA
    455373c View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/new-assigns-check' into new-assi… 

    …gns-check
    @JustusAdam
    JustusAdam committed Dec 26, 2023
    Configuration menu
    Copy the full SHA
    68a7f6e View commit details
    Browse the repository at this point in the history

Commits on Jan 29, 2024

  1. Addressing code review comments 

    Moved contracts code gen functions to separate module
Moved `Pointer` trait to `internal` module
Remove channel based modifies contract communication
    @JustusAdam
    JustusAdam committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    0980cbc View commit details
    Browse the repository at this point in the history

  2. Copyright

    @JustusAdam
    JustusAdam committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    fac45b6 View commit details
    Browse the repository at this point in the history

  3. Clippy suggestions

    @JustusAdam
    JustusAdam committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    96d4b12 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'fork/main' into new-assigns-check

    @JustusAdam
    JustusAdam committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    63d2d7a View commit details
    Browse the repository at this point in the history

  5. Update error reporting

    @JustusAdam
    JustusAdam committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    d105b87 View commit details
    Browse the repository at this point in the history

Commits on Jan 30, 2024

  1. Fixing manes used by contracts metadata

    @JustusAdam
    JustusAdam committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    5eab701 View commit details
    Browse the repository at this point in the history

  2. Fix test case

    @JustusAdam
    JustusAdam committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    4bd7583 View commit details
    Browse the repository at this point in the history

Commits on Jan 31, 2024

  1. Formatting

    @JustusAdam
    JustusAdam committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    0a4503a View commit details
    Browse the repository at this point in the history

  2. Clippy complained

    @JustusAdam
    JustusAdam committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    6414e22 View commit details
    Browse the repository at this point in the history

  3. Whoops

    @JustusAdam
    JustusAdam committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    6bbbb24 View commit details
    Browse the repository at this point in the history

  4. Name the other Rc test case 'fixme'

    @JustusAdam
    JustusAdam committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    9b17d94 View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2024

  1. Forgot that this now needs formatting

    @JustusAdam
    JustusAdam committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    52e703a View commit details
    Browse the repository at this point in the history

  2. Used the wrong name

    @JustusAdam
    JustusAdam committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    40e3abe View commit details
    Browse the repository at this point in the history

  3. Merge branch 'main' into new-assigns-check

    @feliperodri
    feliperodri authored Feb 1, 2024
    Configuration menu
    Copy the full SHA
    8db7d20 View commit details
    Browse the repository at this point in the history

Commits on Feb 2, 2024

  1. Suggestions from code review

    @JustusAdam
    JustusAdam committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    75a554d View commit details
    Browse the repository at this point in the history

  2. Forgot to stage after renaming

    @JustusAdam
    JustusAdam committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    edd7bf8 View commit details
    Browse the repository at this point in the history

  3. Moving all the contract communication logic into the compiler

    @JustusAdam
    JustusAdam committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    7d08810 View commit details
    Browse the repository at this point in the history

  4. Wrong import

    @JustusAdam
    JustusAdam committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    1807020 View commit details
    Browse the repository at this point in the history