-
Notifications
You must be signed in to change notification settings - Fork 261
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.
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
Use CanCall everywhere #5654
base: master
Are you sure you want to change the base?
Use CanCall everywhere #5654
Commits on Jun 11, 2024
-
Configuration menu - View commit details
-
Copy full SHA for e5e3e7c - Browse repository at this point
Copy the full SHA e5e3e7cView commit details -
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
Configuration menu - View commit details
-
Copy full SHA for 0ad2411 - Browse repository at this point
Copy the full SHA 0ad2411View commit details -
Configuration menu - View commit details
-
Copy full SHA for facdbef - Browse repository at this point
Copy the full SHA facdbefView commit details -
Configuration menu - View commit details
-
Copy full SHA for 2cd6a52 - Browse repository at this point
Copy the full SHA 2cd6a52View commit details
Commits on Jun 12, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 702c222 - Browse repository at this point
Copy the full SHA 702c222View commit details -
Configuration menu - View commit details
-
Copy full SHA for 86738d6 - Browse repository at this point
Copy the full SHA 86738d6View commit details -
Configuration menu - View commit details
-
Copy full SHA for e712995 - Browse repository at this point
Copy the full SHA e712995View commit details -
Configuration menu - View commit details
-
Copy full SHA for bf0ec2c - Browse repository at this point
Copy the full SHA bf0ec2cView commit details -
Configuration menu - View commit details
-
Copy full SHA for 73d0b5c - Browse repository at this point
Copy the full SHA 73d0b5cView commit details -
Configuration menu - View commit details
-
Copy full SHA for 13aa0d9 - Browse repository at this point
Copy the full SHA 13aa0d9View commit details -
Configuration menu - View commit details
-
Copy full SHA for e7e6c61 - Browse repository at this point
Copy the full SHA e7e6c61View commit details
Commits on Jun 13, 2024
-
Configuration menu - View commit details
-
Copy full SHA for e1e695b - Browse repository at this point
Copy the full SHA e1e695bView commit details -
Configuration menu - View commit details
-
Copy full SHA for 500ff5c - Browse repository at this point
Copy the full SHA 500ff5cView commit details
Commits on Jun 14, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 79d3291 - Browse repository at this point
Copy the full SHA 79d3291View commit details
Commits on Jun 17, 2024
-
Configuration menu - View commit details
-
Copy full SHA for ecef1e7 - Browse repository at this point
Copy the full SHA ecef1e7View commit details -
Carve pre/post-conditions up into separate conjuncts
dafny4/Fstar-QuickSort.dfy
Configuration menu - View commit details
-
Copy full SHA for 8f5822f - Browse repository at this point
Copy the full SHA 8f5822fView commit details
Commits on Jun 20, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 5e697d2 - Browse repository at this point
Copy the full SHA 5e697d2View commit details -
Configuration menu - View commit details
-
Copy full SHA for 8cc0ba6 - Browse repository at this point
Copy the full SHA 8cc0ba6View commit details
Commits on Jul 16, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 8f0b321 - Browse repository at this point
Copy the full SHA 8f0b321View commit details -
Configuration menu - View commit details
-
Copy full SHA for 2dc5fa4 - Browse repository at this point
Copy the full SHA 2dc5fa4View commit details -
Configuration menu - View commit details
-
Copy full SHA for ea774a5 - Browse repository at this point
Copy the full SHA ea774a5View commit details -
Configuration menu - View commit details
-
Copy full SHA for 466c1b8 - Browse repository at this point
Copy the full SHA 466c1b8View commit details -
Configuration menu - View commit details
-
Copy full SHA for 171939e - Browse repository at this point
Copy the full SHA 171939eView commit details -
Configuration menu - View commit details
-
Copy full SHA for c7222b6 - Browse repository at this point
Copy the full SHA c7222b6View commit details -
Configuration menu - View commit details
-
Copy full SHA for 94a0ccc - Browse repository at this point
Copy the full SHA 94a0cccView commit details
Commits on Jul 17, 2024
-
Configuration menu - View commit details
-
Copy full SHA for f059ffd - Browse repository at this point
Copy the full SHA f059ffdView commit details -
Configuration menu - View commit details
-
Copy full SHA for d63ff0a - Browse repository at this point
Copy the full SHA d63ff0aView commit details
Commits on Jul 20, 2024
-
Configuration menu - View commit details
-
Copy full SHA for f7bf313 - Browse repository at this point
Copy the full SHA f7bf313View commit details -
Configuration menu - View commit details
-
Copy full SHA for 460e400 - Browse repository at this point
Copy the full SHA 460e400View commit details -
Add CanCall assumptions to generated let function
Fixes comp/Comprehensions.dfy
Configuration menu - View commit details
-
Copy full SHA for 09be550 - Browse repository at this point
Copy the full SHA 09be550View commit details -
Configuration menu - View commit details
-
Copy full SHA for 87b6f0f - Browse repository at this point
Copy the full SHA 87b6f0fView commit details
Commits on Jul 22, 2024
-
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
Configuration menu - View commit details
-
Copy full SHA for 3127da2 - Browse repository at this point
Copy the full SHA 3127da2View commit details -
Configuration menu - View commit details
-
Copy full SHA for 8bba9a1 - Browse repository at this point
Copy the full SHA 8bba9a1View commit details -
Configuration menu - View commit details
-
Copy full SHA for 567c667 - Browse repository at this point
Copy the full SHA 567c667View commit details -
Configuration menu - View commit details
-
Copy full SHA for 7db4ffc - Browse repository at this point
Copy the full SHA 7db4ffcView commit details -
Configuration menu - View commit details
-
Copy full SHA for e5c91dd - Browse repository at this point
Copy the full SHA e5c91ddView commit details
Commits on Jul 23, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 1379380 - Browse repository at this point
Copy the full SHA 1379380View commit details -
Configuration menu - View commit details
-
Copy full SHA for 3a8307e - Browse repository at this point
Copy the full SHA 3a8307eView commit details
Commits on Jul 30, 2024
-
Configuration menu - View commit details
-
Copy full SHA for a9b195a - Browse repository at this point
Copy the full SHA a9b195aView commit details -
Configuration menu - View commit details
-
Copy full SHA for afdb5c5 - Browse repository at this point
Copy the full SHA afdb5c5View commit details -
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
Configuration menu - View commit details
-
Copy full SHA for b657928 - Browse repository at this point
Copy the full SHA b657928View commit details
Commits on Sep 27, 2024
-
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
Configuration menu - View commit details
-
Copy full SHA for 1cb2672 - Browse repository at this point
Copy the full SHA 1cb2672View commit details -
Configuration menu - View commit details
-
Copy full SHA for bcc497b - Browse repository at this point
Copy the full SHA bcc497bView commit details
Commits on Oct 3, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 349a2ea - Browse repository at this point
Copy the full SHA 349a2eaView commit details -
Configuration menu - View commit details
-
Copy full SHA for 5cee693 - Browse repository at this point
Copy the full SHA 5cee693View commit details -
Add CanCall assumptions in short-circuit WF-result checks
Test case that discovered problem: dafny0/MoForallCompilation.dfy
Configuration menu - View commit details
-
Copy full SHA for 0a45814 - Browse repository at this point
Copy the full SHA 0a45814View commit details -
Configuration menu - View commit details
-
Copy full SHA for 8973a0a - Browse repository at this point
Copy the full SHA 8973a0aView commit details -
Configuration menu - View commit details
-
Copy full SHA for 9ec69b2 - Browse repository at this point
Copy the full SHA 9ec69b2View commit details
Commits on Oct 4, 2024
-
Configuration menu - View commit details
-
Copy full SHA for ceff013 - Browse repository at this point
Copy the full SHA ceff013View commit details -
Configuration menu - View commit details
-
Copy full SHA for f4c9588 - Browse repository at this point
Copy the full SHA f4c9588View commit details
Commits on Oct 8, 2024
-
Without general traits, the new resolver infers the type of `fetch` to be `Ins?`, which causes a null dereference in `run()`.
Configuration menu - View commit details
-
Copy full SHA for d7a2754 - Browse repository at this point
Copy the full SHA d7a2754View commit details
Commits on Oct 9, 2024
-
Avoid triggers with nullary functions
Test case: git-issues/git-issue-405.dfy
Configuration menu - View commit details
-
Copy full SHA for b8332aa - Browse repository at this point
Copy the full SHA b8332aaView commit details -
Configuration menu - View commit details
-
Copy full SHA for 09b3930 - Browse repository at this point
Copy the full SHA 09b3930View commit details -
Configuration menu - View commit details
-
Copy full SHA for 96cd511 - Browse repository at this point
Copy the full SHA 96cd511View commit details -
Configuration menu - View commit details
-
Copy full SHA for 41fa183 - Browse repository at this point
Copy the full SHA 41fa183View commit details
Commits on Oct 10, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 522513f - Browse repository at this point
Copy the full SHA 522513fView commit details
Commits on Oct 12, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 5f3cfdc - Browse repository at this point
Copy the full SHA 5f3cfdcView commit details -
Configuration menu - View commit details
-
Copy full SHA for cd9d205 - Browse repository at this point
Copy the full SHA cd9d205View commit details
Commits on Oct 18, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 8547807 - Browse repository at this point
Copy the full SHA 8547807View commit details -
Configuration menu - View commit details
-
Copy full SHA for c164820 - Browse repository at this point
Copy the full SHA c164820View commit details