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

WIP: Iterator tracking issues #980

Open
wants to merge 45 commits into
base: master
Choose a base branch
from
Open

WIP: Iterator tracking issues #980

wants to merge 45 commits into from

Commits on Apr 28, 2022

  1. Adjust copy check in environment to better handle regions

    @vl0w
    vl0w committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    4caee3a View commit details
    Browse the repository at this point in the history

  2. Maybe we need to handle TyKind::Ref differently?

    @vl0w
    vl0w committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    ed7dffd View commit details
    Browse the repository at this point in the history

  3. Support associated types in copy check

    @vl0w
    vl0w committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    03b3640 View commit details
    Browse the repository at this point in the history

  4. Pass type with binder to type_is_copy to better account for regions

    @vl0w
    vl0w committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    138d98e View commit details
    Browse the repository at this point in the history

  5. Normalize function signature in PureFunctionEncoder to account for as… 

    …sociated types
    @vl0w
    vl0w committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    a408861 View commit details
    Browse the repository at this point in the history

  6. Remove check for validity of pure function in process_encoding_queue

    @vl0w
    vl0w committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    dbbed0d View commit details
    Browse the repository at this point in the history

  7. Erase all regions in copy check

    @vl0w
    vl0w committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    161b956 View commit details
    Browse the repository at this point in the history

  8. Do not perform normalization when there are no projections

    @vl0w
    vl0w committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    eda1445 View commit details
    Browse the repository at this point in the history

  9. Partially undo removal of code in process_encoding_queue.

    @vl0w
    vl0w committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    41aad37 View commit details
    Browse the repository at this point in the history

  10. Rename normalize_to, return original value if normalized value contai… 

    …ns infer types
    @vl0w
    vl0w committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    e2a5467 View commit details
    Browse the repository at this point in the history

Commits on Apr 29, 2022

  1. Pass ParamEnv to resolve_assoc_types, make it fallible

    @vl0w
    vl0w committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    43a5387 View commit details
    Browse the repository at this point in the history

  2. Small cleanups

    @vl0w
    vl0w committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    b604cd4 View commit details
    Browse the repository at this point in the history

  3. Add custom iterator tests

    @vl0w
    vl0w committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    5dc9705 View commit details
    Browse the repository at this point in the history

  4. Add flag to add experimental iterator support

    @vl0w
    vl0w committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    f8f2859 View commit details
    Browse the repository at this point in the history

  5. Move predicate normalization in constraint solver for better debugging

    @vl0w
    vl0w committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    0da3287 View commit details
    Browse the repository at this point in the history

  6. Do not copy preconditions of base spec to constrained spec

    @vl0w
    vl0w committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    c1cbead View commit details
    Browse the repository at this point in the history

  7. Use predicate_must_hold_modulo_regions when resolving ghost constrain… 

    …ts to account for references in associated types
    @vl0w
    vl0w committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    59bc78c View commit details
    Browse the repository at this point in the history

  8. Handle lifetimes in merge_generics

    @vl0w
    vl0w committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    0af45d7 View commit details
    Browse the repository at this point in the history

Commits on May 2, 2022

  1. Support lifetimes in type models

    @vl0w
    vl0w committed May 2, 2022
    Configuration menu
    Copy the full SHA
    c527dc1 View commit details
    Browse the repository at this point in the history

  2. Relax needs_infer check in Environment::resolve_method_call to ignore… 

    … non-resolved lifetimes
    @vl0w
    vl0w committed May 2, 2022
    Configuration menu
    Copy the full SHA
    c8081fb View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into iterators-feature-flag 

    # Conflicts:
#	prusti-interface/src/environment/mod.rs
#	prusti-viper/src/encoder/mir/specifications/constraints.rs
    @vl0w
    vl0w committed May 2, 2022
    Configuration menu
    Copy the full SHA
    78c51fb View commit details
    Browse the repository at this point in the history

Commits on May 3, 2022

  1. Support lifetimes in type models

    @vl0w
    vl0w committed May 3, 2022
    Configuration menu
    Copy the full SHA
    af55da2 View commit details
    Browse the repository at this point in the history

  2. Add first tests

    @vl0w
    vl0w committed May 3, 2022
    Configuration menu
    Copy the full SHA
    8c7a2ab View commit details
    Browse the repository at this point in the history

Commits on May 4, 2022

  1. Verification of Iter in while loop

    @vl0w
    vl0w committed May 4, 2022
    Configuration menu
    Copy the full SHA
    fa1c14a View commit details
    Browse the repository at this point in the history

  2. Create custom Copy/Clone impls for type models (do not derive them)

    @vl0w
    vl0w committed May 4, 2022
    Configuration menu
    Copy the full SHA
    5e396ff View commit details
    Browse the repository at this point in the history

  3. Adjust flag docs for iterator killswitch

    @vl0w
    vl0w committed May 4, 2022
    Configuration menu
    Copy the full SHA
    3afba7c View commit details
    Browse the repository at this point in the history

Commits on May 6, 2022

  1. Normalize substs in Environment::resolve_method_call to account for n… 

    …on-resolved associated types
    @vl0w
    vl0w committed May 6, 2022
    Configuration menu
    Copy the full SHA
    70e5b0f View commit details
    Browse the repository at this point in the history

Commits on May 8, 2022

  1. Fix typo

    @vl0w
    vl0w committed May 8, 2022
    Configuration menu
    Copy the full SHA
    ed1a7a5 View commit details
    Browse the repository at this point in the history

Commits on May 10, 2022

  1. Support associated types in quantifiers

    @vl0w
    vl0w committed May 10, 2022
    Configuration menu
    Copy the full SHA
    d1d4953 View commit details
    Browse the repository at this point in the history

  2. Remove dead comment in any_type_needs_infer

    @vl0w
    vl0w committed May 10, 2022
    Configuration menu
    Copy the full SHA
    7e7bde4 View commit details
    Browse the repository at this point in the history

Commits on May 17, 2022

  1. Remove dead code

    @vl0w
    vl0w committed May 17, 2022
    Configuration menu
    Copy the full SHA
    e3bbbd9 View commit details
    Browse the repository at this point in the history

Commits on May 23, 2022

  1. Merge branch 'master' into iterators-feature-flag 

    # Conflicts:
#	prusti-common/src/config.rs
#	prusti-interface/src/environment/mod.rs
    @vl0w
    vl0w committed May 23, 2022
    Configuration menu
    Copy the full SHA
    8e05591 View commit details
    Browse the repository at this point in the history

Commits on May 30, 2022

  1. Merge branch 'master' into iterators-feature-flag 

    # Conflicts:
#	prusti-interface/src/specs/typed.rs
    @vl0w
    vl0w committed May 30, 2022
    Configuration menu
    Copy the full SHA
    116bcd6 View commit details
    Browse the repository at this point in the history

Commits on Jun 12, 2022

  1. fix for viperproject#1033 with test cases

    @Pointerbender @Aurel300
    Pointerbender authored and Aurel300 committed Jun 12, 2022
    Configuration menu
    Copy the full SHA
    f16f646 View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2022

  1. snapshot equality

    @Aurel300
    Aurel300 committed Jul 12, 2022
    Configuration menu
    Copy the full SHA
    96ee8b9 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2022

  1. remove special Fn*::call* treatment

    @Aurel300
    Aurel300 committed Jul 18, 2022
    Configuration menu
    Copy the full SHA
    414e081 View commit details
    Browse the repository at this point in the history

  2. test closures using type-dependent contracts

    @Aurel300
    Aurel300 committed Jul 18, 2022
    Configuration menu
    Copy the full SHA
    2b6d632 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2022

  1. Merge remote-tracking branch 'upstream/master' into iterators-feature… 

    …-flag
    @Aurel300
    Aurel300 committed Jul 19, 2022
    Configuration menu
    Copy the full SHA
    9142078 View commit details
    Browse the repository at this point in the history

Commits on Jul 20, 2022

  1. fix

    @Aurel300
    Aurel300 committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    186e97e View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2022

  1. Merge remote-tracking branch 'upstream/master' into iterators-feature… 

    …-flag
    @Aurel300
    Aurel300 committed Jul 22, 2022
    Configuration menu
    Copy the full SHA
    8ed4eb2 View commit details
    Browse the repository at this point in the history

Commits on Jul 27, 2022

  1. erase regions less eagerly for method calls

    @Aurel300
    Aurel300 committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    dbd4d2d View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master' into iterators-feature… 

    …-flag
    @Aurel300
    Aurel300 committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    1eaa7d0 View commit details
    Browse the repository at this point in the history

  3. fix

    @Aurel300
    Aurel300 committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    c74215b View commit details
    Browse the repository at this point in the history

Commits on Jul 29, 2022

  1. Merge remote-tracking branch 'upstream/master' into iterators-feature… 

    …-flag
    @Aurel300
    Aurel300 committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    e9e5c78 View commit details
    Browse the repository at this point in the history

  2. another unsafe core proof workaround for trait resolution

    @Aurel300
    Aurel300 committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    fa449f9 View commit details
    Browse the repository at this point in the history