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

Properly check if types may contain references #1924

Merged
merged 15 commits into from
Apr 28, 2022
Merged

Properly check if types may contain references #1924

merged 15 commits into from
Apr 28, 2022

Commits on Mar 21, 2022

  1. fix: Checking of MayInvolveReferences

    @RustanLeino
    RustanLeino committed Mar 21, 2022
    Configuration menu
    Copy the full SHA
    8c95036 View commit details
    Browse the repository at this point in the history

  2. fix: Replace (buggy) IsAllocFree with !MayContainReferences

    @RustanLeino
    RustanLeino committed Mar 21, 2022
    Configuration menu
    Copy the full SHA
    af08d8e View commit details
    Browse the repository at this point in the history

  3. Add tests 

    Fixes dafny-lang#1419
    @RustanLeino
    RustanLeino committed Mar 21, 2022
    Configuration menu
    Copy the full SHA
    5b940ce View commit details
    Browse the repository at this point in the history

  4. Update release notes

    @RustanLeino
    RustanLeino committed Mar 21, 2022
    Configuration menu
    Copy the full SHA
    28b7ebb View commit details
    Browse the repository at this point in the history

Commits on Mar 24, 2022

  1. fix: Compute MayInvolveReference correctly for datatypes 

    The Schorr-Waite test programs are not allowed by the new rules. To sort this out, Dafny needs a more flexible mechanism to indicate that quantifiers only quantify over allocated state. I will add this mechanism in a separate PR and then return to this one.
    @RustanLeino
    RustanLeino committed Mar 24, 2022
    Configuration menu
    Copy the full SHA
    270af06 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into issue-1419

    @RustanLeino
    RustanLeino committed Mar 24, 2022
    Configuration menu
    Copy the full SHA
    ae9784b View commit details
    Browse the repository at this point in the history

Commits on Mar 26, 2022

  1. Merge branch 'master' into issue-1419

    @RustanLeino
    RustanLeino committed Mar 26, 2022
    Configuration menu
    Copy the full SHA
    a55dded View commit details
    Browse the repository at this point in the history

  2. Add :older attributes 

    These `:older` attributes on `ReachableVia` will once again allow the `SchorrWaite*.dfy` tests, as soon as dafny-lang#1936 is merged.
    @RustanLeino
    RustanLeino committed Mar 26, 2022
    Configuration menu
    Copy the full SHA
    bdf44fe View commit details
    Browse the repository at this point in the history

Commits on Mar 30, 2022

  1. Move ComputeMayInvolveReferences implementations closer to leaf AST t… 

    …ypes
    @RustanLeino
    RustanLeino committed Mar 30, 2022
    Configuration menu
    Copy the full SHA
    d12f190 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into issue-1419

    @RustanLeino
    RustanLeino committed Mar 30, 2022
    Configuration menu
    Copy the full SHA
    c3609e7 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into issue-1419

    @RustanLeino
    RustanLeino authored Mar 30, 2022
    Configuration menu
    Copy the full SHA
    b46d522 View commit details
    Browse the repository at this point in the history

Commits on Apr 25, 2022

  1. Merge branch 'master' into issue-1419 

    # Conflicts:
#	RELEASE_NOTES.md
    @RustanLeino
    RustanLeino committed Apr 25, 2022
    Configuration menu
    Copy the full SHA
    4519dc5 View commit details
    Browse the repository at this point in the history

Commits on Apr 28, 2022

  1. Merge branch 'master' into issue-1419 

    # Conflicts:
#	RELEASE_NOTES.md
#	Source/Dafny/Resolver.cs
    @RustanLeino
    RustanLeino committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    9d6467c View commit details
    Browse the repository at this point in the history

  2. Adjust tests for ‘older’ and for new error messages

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

  3. Merge branch 'master' into issue-1419

    @cpitclaudel
    cpitclaudel authored Apr 28, 2022
    Configuration menu
    Copy the full SHA
    93bc6d5 View commit details
    Browse the repository at this point in the history