Convert tests to also exercise new type system #4626
Conversation
# Conflicts: # Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs # Source/DafnyCore/Compilers/GoLang/Compiler-go.cs # Source/DafnyCore/Compilers/Java/Compiler-java.cs # Source/DafnyCore/Compilers/SinglePassCompiler.cs # Test/dafny0/GhostAllocations.dfy.expect # Test/git-issues/git-issue-1252.dfy.expect
As required by match expression in Test/dafny0/Datatypes.dfy
# Conflicts: # Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs # Source/DafnyCore/Compilers/SinglePassCompiler.cs
# Conflicts: # Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
# Conflicts: # Source/DafnyCore/Compilers/Java/Compiler-java.cs # Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs # Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs # Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs # Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs # Source/DafnyCore/Resolver/PreType/PreTypeResolver.Match.cs # Test/dafny0/OnDemandResolutionOrdering.dfy.expect # Test/traits/GeneralTraitsCompile.dfy # Test/traits/GeneralTraitsCompile.dfy.expect
# Conflicts: # Source/DafnyCore/Resolver/PreType/Flows.cs
…n refinement module
# Conflicts: # Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs # Test/dafny0/Termination.dfy # Test/traits/GeneralTraitsCompile.dfy # Test/traits/NonReferenceTraitsCompile.dfy
# Conflicts: # Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy
A test for this is in `git-issues/git-issue-4315.dfy`
| @@ -1,5 +1,5 @@ | |||
| // NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108 | |||
| // RUN: %testDafnyForEachCompiler "%s" --refresh-exit-code=0 -- --relax-definite-assignment --spill-translation --unicode-char:false | |||
| // RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false | |||
There was a problem hiding this comment.
Was this change made just for the sake of consistency, or does it actually affect the meaning of the command?
There was a problem hiding this comment.
There's no difference in meaning. I changed all of these to put the "%s" at the end (before the --, if any).
| @@ -963,6 +963,38 @@ module StaticReceivers { | |||
| } | |||
|
|
|||
|
|
|||
| /**************************************************************************************** | |||
There was a problem hiding this comment.
Does this need to be resolved before merging the PR?
There was a problem hiding this comment.
Thanks. I cleaned this up, but am leaving two of these to-do problems in the test file. I'm looking into one of them now (but as a separate PR, once I resolve it).
| Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<ActualBinding> args, | ||
| ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true) { | ||
| ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true, bool specialOpaqueHackAllowance = false) { |
There was a problem hiding this comment.
It would be nice to have this change in a separate PR, but I don't think it's a blocker.
There was a problem hiding this comment.
You're right, this change does not belong in this PR. I'm moving it to a separate one and am reverting git-issue-4315.dfy to just run with the old resolver.
There was a problem hiding this comment.
The separate PR is #4733
…er does" This reverts commit 483af6c. This change has been moved to a separate PR: dafny-lang#4733
The changes in this PR concern only the test suite. In particular, it converts some 500 test files to run both the old resolver and the new resolver.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.