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

Use CanCall everywhere #5654

Draft
wants to merge 60 commits into
base: master
Choose a base branch
from
Draft

Use CanCall everywhere #5654

wants to merge 60 commits into from

Commits on Jun 11, 2024

  1. Snapshot changes

    @RustanLeino
    RustanLeino committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    e5e3e7c View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into can-call-diff 

    # Conflicts:
#	Source/Dafny/Verifier/Translator.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370.dfy
#	Test/dafny0/FunctionSpecifications.dfy.expect
#	Test/git-issues/git-issue-370.dfy.expect
    @RustanLeino
    RustanLeino committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    0ad2411 View commit details
    Browse the repository at this point in the history

  3. Fix parameter order to CanCallAssumption

    @RustanLeino
    RustanLeino committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    facdbef View commit details
    Browse the repository at this point in the history

  4. Manually merge in the changes from the old Translator.cs

    @RustanLeino
    RustanLeino committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    2cd6a52 View commit details
    Browse the repository at this point in the history

Commits on Jun 12, 2024

  1. Fix merge

    @RustanLeino
    RustanLeino committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    702c222 View commit details
    Browse the repository at this point in the history

  2. Add FreeRequires/FreeEnsures helper methods

    @RustanLeino
    RustanLeino committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    86738d6 View commit details
    Browse the repository at this point in the history

  3. chore: Remove deprecated semi-colons

    @RustanLeino
    RustanLeino committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    e712995 View commit details
    Browse the repository at this point in the history

  4. Restore FunctionSpecification.dfy

    @RustanLeino
    RustanLeino committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    bf0ec2c View commit details
    Browse the repository at this point in the history

  5. Move generation of req==>CanCall axiom

    @RustanLeino
    RustanLeino committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    73d0b5c View commit details
    Browse the repository at this point in the history

  6. Replace kv parameter by alwaysAssume option in Free-Requires/Ensures

    @RustanLeino
    RustanLeino committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    13aa0d9 View commit details
    Browse the repository at this point in the history

  7. Don’t add CanCall _inside_ frame condition, but as free precondition

    @RustanLeino
    RustanLeino committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    e7e6c61 View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2024

  1. Assume CanCall of callee frames

    @RustanLeino
    RustanLeino committed Jun 13, 2024
    Configuration menu
    Copy the full SHA
    e1e695b View commit details
    Browse the repository at this point in the history

  2. chore: Remove deprecated semi-colons

    @RustanLeino
    RustanLeino committed Jun 13, 2024
    Configuration menu
    Copy the full SHA
    500ff5c View commit details
    Browse the repository at this point in the history

Commits on Jun 14, 2024

  1. Generate CanCall assumptions for result of calc

    @RustanLeino
    RustanLeino committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    79d3291 View commit details
    Browse the repository at this point in the history

Commits on Jun 17, 2024

  1. Generate CanCall assumptions for array/seq init expression

    @RustanLeino
    RustanLeino committed Jun 17, 2024
    Configuration menu
    Copy the full SHA
    ecef1e7 View commit details
    Browse the repository at this point in the history

  2. Carve pre/post-conditions up into separate conjuncts 

    dafny4/Fstar-QuickSort.dfy
    @RustanLeino
    RustanLeino committed Jun 17, 2024
    Configuration menu
    Copy the full SHA
    8f5822f View commit details
    Browse the repository at this point in the history

Commits on Jun 20, 2024

  1. Fix null dereference

    @RustanLeino
    RustanLeino committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    5e697d2 View commit details
    Browse the repository at this point in the history

  2. chore: Remove stale comment

    @RustanLeino
    RustanLeino committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    8cc0ba6 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2024

  1. Strip any box/unbox around trigger terms

    @RustanLeino
    RustanLeino committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    8f0b321 View commit details
    Browse the repository at this point in the history

  2. Fix casts in test case

    @RustanLeino
    RustanLeino committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    2dc5fa4 View commit details
    Browse the repository at this point in the history

  3. Fix ConjunctsOf to not drop labels

    @RustanLeino
    RustanLeino committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    ea774a5 View commit details
    Browse the repository at this point in the history

  4. Add CanCalls to primed version of comprehension uniqueness check

    @RustanLeino
    RustanLeino committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    466c1b8 View commit details
    Browse the repository at this point in the history

  5. Reflect change in error output ordering

    @RustanLeino
    RustanLeino committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    171939e View commit details
    Browse the repository at this point in the history

  6. Fix Conjuncts all to include type of new LetExpr’s

    @RustanLeino
    RustanLeino committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    c7222b6 View commit details
    Browse the repository at this point in the history

  7. Add CanCall assumptions to subset-constraint checks

    @RustanLeino
    RustanLeino committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    94a0ccc View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2024

  1. Restructure CanCallOptions and make allowances for overriding functions

    @RustanLeino
    RustanLeino committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    f059ffd View commit details
    Browse the repository at this point in the history

  2. Add CanCan antecedent to “r” component of function handles

    @RustanLeino
    RustanLeino committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    d63ff0a View commit details
    Browse the repository at this point in the history

Commits on Jul 20, 2024

  1. Remove deprecation

    @RustanLeino
    RustanLeino committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    f7bf313 View commit details
    Browse the repository at this point in the history

  2. Use :induction instead of /induction:3

    @RustanLeino
    RustanLeino committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    460e400 View commit details
    Browse the repository at this point in the history

  3. Add CanCall assumptions to generated let function 

    Fixes comp/Comprehensions.dfy
    @RustanLeino
    RustanLeino committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    09be550 View commit details
    Browse the repository at this point in the history

  4. Adjust test case, which is now passing

    @RustanLeino
    RustanLeino committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    87b6f0f View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2024

  1. Incorporate CanCall into newtype/subset-type $Is axioms 

    This helped many tests go through, including:
* autoRevealDependencies/subset-types.dfy
* git-issues/git-issue-1479.dfy
* git-issues/git-issue-362.dfy
    @RustanLeino
    RustanLeino committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    3127da2 View commit details
    Browse the repository at this point in the history

  2. Update order of error messages in expect file

    @RustanLeino
    RustanLeino committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    8bba9a1 View commit details
    Browse the repository at this point in the history

  3. Remove a redundant test file

    @RustanLeino
    RustanLeino committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    567c667 View commit details
    Browse the repository at this point in the history

  4. Adjust test output

    @RustanLeino
    RustanLeino committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    7db4ffc View commit details
    Browse the repository at this point in the history

  5. Fix parameters to CanCall function in override axiom

    @RustanLeino
    RustanLeino committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    e5c91dd View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2024

  1. Change override axiom to use CanCall

    @RustanLeino
    RustanLeino committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    1379380 View commit details
    Browse the repository at this point in the history

  2. Adjust resource limit (down) to make test pass

    @RustanLeino
    RustanLeino committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    3a8307e View commit details
    Browse the repository at this point in the history

Commits on Jul 30, 2024

  1. Fix typo in comments

    @RustanLeino
    RustanLeino committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    a9b195a View commit details
    Browse the repository at this point in the history

  2. Add workaround for incorrect partial-arrow constraint

    @RustanLeino
    RustanLeino committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    afdb5c5 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into can-call-everywhere 

    # Conflicts:
#	Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.cs
    @RustanLeino
    RustanLeino committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    b657928 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2024

  1. Merge branch 'master' into can-call-everywhere 

    # Conflicts:
#	Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.Types.cs
#	Source/DafnyCore/Verifier/BoogieGenerator.cs
    @RustanLeino
    RustanLeino committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    1cb2672 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into can-call-everywhere

    @RustanLeino
    RustanLeino committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    bcc497b View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2024

  1. Fix bad refactoring

    @RustanLeino
    RustanLeino committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    349a2ea View commit details
    Browse the repository at this point in the history

  2. Adjust test and answer

    @RustanLeino
    RustanLeino committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    5cee693 View commit details
    Browse the repository at this point in the history

  3. Add CanCall assumptions in short-circuit WF-result checks 

    Test case that discovered problem: dafny0/MoForallCompilation.dfy
    @RustanLeino
    RustanLeino committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    0a45814 View commit details
    Browse the repository at this point in the history

  4. Fix implementations of Disjuncts and Conjuncts

    @RustanLeino
    RustanLeino committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    8973a0a View commit details
    Browse the repository at this point in the history

  5. Change \d to [0-9], since the former apparently isn’t always supported

    @RustanLeino
    RustanLeino committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    9ec69b2 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2024

  1. Merge branch 'master' into can-call-everywhere

    @RustanLeino
    RustanLeino committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    ceff013 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into can-call-everywhere

    @RustanLeino
    RustanLeino committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    f4c9588 View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2024

  1. Adjust test and answer 

    Without general traits, the new resolver infers the type of `fetch` to be `Ins?`, which causes a null dereference in `run()`.
    @RustanLeino
    RustanLeino committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    d7a2754 View commit details
    Browse the repository at this point in the history

Commits on Oct 9, 2024

  1. Avoid triggers with nullary functions 

    Test case: git-issues/git-issue-405.dfy
    @RustanLeino
    RustanLeino committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    b8332aa View commit details
    Browse the repository at this point in the history

  2. chore: Remove old syntax

    @RustanLeino
    RustanLeino committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    09b3930 View commit details
    Browse the repository at this point in the history

  3. Reorder error output

    @RustanLeino
    RustanLeino committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    96cd511 View commit details
    Browse the repository at this point in the history

  4. Update RUs in test outputs

    @RustanLeino
    RustanLeino committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    41fa183 View commit details
    Browse the repository at this point in the history

Commits on Oct 10, 2024

  1. Separate assertions into separate methods to avoid Z3 ordering problem

    @RustanLeino
    RustanLeino committed Oct 10, 2024
    Configuration menu
    Copy the full SHA
    522513f View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2024

  1. chore: Improve trigger/induction code

    @RustanLeino
    RustanLeino committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    5f3cfdc View commit details
    Browse the repository at this point in the history

  2. Compute triggers for automatic induction

    @RustanLeino
    RustanLeino committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    cd9d205 View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2024

  1. Merge remote-tracking branch 'origin/master' into can-call-everywhere

    @keyboardDrummer
    keyboardDrummer committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    8547807 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into can-call-everywhere

    @keyboardDrummer
    keyboardDrummer committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    c164820 View commit details
    Browse the repository at this point in the history