Merge branch 'master' into issue-6043

# Conflicts:
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-847.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Naked.dfy.expect

Source/Dafny.sln

@@ -43,6 +43,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Scripts", "Scripts\Scripts.csproj", "{3FAB051A-1745-497B-B4C0-D49194BB5D32}"
+EndProject
 EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -130,6 +132,10 @@ Global
 		{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.Build.0 = Release|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Release|Any CPU.Build.0 = Release|Any CPU
 	EndGlobalSection
 	GlobalSection(SolutionProperties) = preSolution
 		HideSolutionNode = FALSE

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -2490,6 +2490,7 @@ public override string PublicIdProtect(string name) {
         case "ToString":
         case "GetHashCode":
         case "Main":
+        case "Default":
           return "_" + name;
         default:
           return name;

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -2515,7 +2515,7 @@ private string IdName(Declaration decl) {
         // Don't use Go_ because Capitalize might use it and we know there's a conflict
         return "Go__" + decl.GetCompileName(Options);
       } else {
-        return Capitalize(decl.GetCompileName(Options));
+        return IdProtect(Capitalize(decl.GetCompileName(Options)));
       }
     }
 
@@ -2579,6 +2579,7 @@ public override string PublicIdProtect(string name) {
         case "String":
         case "Equals":
         case "EqualsGeneric":
+        case "Default":
 
         // Built-in types (can also be used as functions)
         case "bool":

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -2440,6 +2440,7 @@ private static string PublicIdProtectAux(string name) {
         case "toString":
         case "equals":
         case "hashCode":
+        case "Default":
           return name + "_"; // TODO: figure out what to do here (C# uses @, Go uses _, JS uses _$$_)
         default:
           return name; // Package name is not a keyword, so it can be used

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -3327,7 +3327,7 @@ internal void ResolveActualParameters(ActualBindings bindings, List<Formal> form
             whatKind + (context is Method ? " in-parameter" : " parameter"));
 
           AddAssignableConstraint(
-            callTok /* TODO should be b.Actual.Origin */, formal.Type.Subst(typeMap), b.Actual.Type,
+            b.Actual.Origin, formal.Type.Subst(typeMap), b.Actual.Type,
             $"incorrect argument type {what} (expected {{0}}, found {{1}})");
         } else if (formal.DefaultValue != null) {
           // Note, in the following line, "substMap" is passed in, but it hasn't been fully filled in until the
@@ -5916,8 +5916,7 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext
           }
           if (callee != null) {
             // produce a FunctionCallExpr instead of an ApplyExpr(MemberSelectExpr)
-            // TODO use e.Origin instead of e.Lhs.Origin
-            var rr = new FunctionCallExpr(new OverrideCenter(e.Origin, e.Lhs.Origin.Center), mse.MemberNameNode, mse.Obj, e.Origin, e.CloseParen, e.Bindings, atLabel) {
+            var rr = new FunctionCallExpr(e.Origin, mse.MemberNameNode, mse.Obj, e.Origin, e.CloseParen, e.Bindings, atLabel) {
               Function = callee,
               TypeApplication_AtEnclosingClass = mse.TypeApplicationAtEnclosingClass,
               TypeApplication_JustFunction = mse.TypeApplicationJustMember

Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs

@@ -127,7 +127,7 @@ internal void ResolveActualParameters(ActualBindings bindings, List<Formal> form
             whatKind + (context is Method ? " in-parameter" : " parameter"));
 
           Constraints.AddSubtypeConstraint(
-            formal.PreType.Substitute(typeMap), b.Actual.PreType, callTok /* TODO should be b.Actual.Origin */,
+            formal.PreType.Substitute(typeMap), b.Actual.PreType, b.Actual.Origin,
             $"incorrect argument type {what} (expected {{0}}, found {{1}})");
         } else if (formal.DefaultValue != null) {
           // Note, in the following line, "substMap" is passed in, but it hasn't been fully filled in until the

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -1756,8 +1756,7 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext
           }
           if (callee != null) {
             // resolve as a FunctionCallExpr instead of as an ApplyExpr(MemberSelectExpr)
-            // TODO use e.Origin instead of e.Lhs.Origin
-            var rr = new FunctionCallExpr(e.Lhs.Origin, mse.MemberNameNode, mse.Obj, e.Origin, e.CloseParen, e.Bindings, atLabel) {
+            var rr = new FunctionCallExpr(e.Origin, mse.MemberNameNode, mse.Obj, e.Origin, e.CloseParen, e.Bindings, atLabel) {
               Function = callee,
               PreTypeApplication_AtEnclosingClass = mse.PreTypeApplicationAtEnclosingClass,
               PreTypeApplication_JustFunction = mse.PreTypeApplicationJustMember

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -1665,9 +1665,13 @@ private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieSt
         }
       }
 
-      var kv = etran.TrAttributes(m.Attributes, null);
 
+      var kv = etran.TrAttributes(m.Attributes, null);
       var tok = m.Origin;
+      var canCalls = traitFrameExps.Concat(classFrameExps)
+        .Select(e => etran.CanCallAssumption(e.E))
+        .Aggregate((Bpl.Expr)Bpl.Expr.True, BplAnd);
+      builder.Add(TrAssumeCmd(tok, canCalls));
       var oVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$o", Predef.RefType));
       var o = new Boogie.IdentifierExpr(tok, oVar);
       var fVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$f", Predef.FieldName(tok)));

Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs

@@ -1,4 +1,4 @@
-using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using System;
 using OmniSharp.Extensions.LanguageServer.Protocol.Document;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using System.Collections.Generic;
@@ -8,7 +8,7 @@
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 using Xunit;
 using Xunit.Abstractions;
-using XunitAssertMessages;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.CodeActions {
   public class CodeActionTest : ClientBasedLanguageServerTest {
@@ -76,6 +76,21 @@ assert x !is B.><
       Assert.Empty(completionList);
     }
 
+    [Fact]
+    public async Task TestAssertFalseNotSuggestingItself() {
+      await TestNoCodeAction(@"
+method NoCodeAction() {
+  assert fal><se;
+}");
+    }
+
+    [Fact]
+    public async Task TestEnsureFalseNotSuggestingItself() {
+      await TestNoCodeAction(@"
+method NoCodeAction() ensures f><alse {
+}", excepted: message => message == "Assert postcondition at return location where it fails");
+    }
+
     [Fact]
     public async Task TestInsertion() {
       await TestCodeAction(@"
@@ -371,6 +386,23 @@ match i {
 
     private static readonly Regex NewlineRegex = new Regex("\r?\n");
 
+    private async Task TestNoCodeAction(string source, Func<string, bool> excepted = null) {
+      await SetUp(o => o.Set(CommonOptionBag.RelaxDefiniteAssignment, true));
+      MarkupTestFile.GetPositionsAndAnnotatedRanges(source.TrimStart(), out var output, out var positions,
+        out var ranges);
+      var documentItem = await CreateOpenAndWaitForResolve(output);
+      var diagnostics = await GetLastDiagnostics(documentItem);
+      Assert.Equal(0, ranges.Count);
+      foreach (var position in positions) {
+        var completionList = await RequestCodeActionAsync(documentItem, new Range(position, position));
+        completionList = excepted == null
+          ? completionList
+          : completionList.Where(completion =>
+            completion.CodeAction is not { Title: var title } || !excepted(title)).ToList();
+        Assert.Empty(completionList);
+      }
+    }
+
     private async Task TestCodeAction(string source) {
       await SetUp(o => o.Set(CommonOptionBag.RelaxDefiniteAssignment, true));
 

Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs

@@ -126,7 +126,9 @@ public override IEnumerable<DafnyCodeActionEdit> GetEdits() {
             assertTree.StatusVerification is GutterVerificationStatus.Error or GutterVerificationStatus.Inconclusive &&
             assertTree.GetAssertion()?.Description is ProofObligationDescription description &&
             description.GetAssertedExpr(options) is { } assertedExpr) {
-        failingExpressions.Add(assertedExpr);
+        if (description.IsImplicit) {
+          failingExpressions.Add(assertedExpr);
+        }
       }
     });
     if (failingExpressions.Count == 0) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass1.dfy.expect

@@ -1,3 +1,3 @@
-ReadPreconditionBypass1.dfy(23,20): Error: function precondition could not be proved
+ReadPreconditionBypass1.dfy(23,25): Error: function precondition could not be proved
 
 Dafny program verifier finished with 1 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect

@@ -17,7 +17,7 @@ at-attributes-typos.dfy(5,0): Error: @AutoContracts attribute cannot be applied
 at-attributes-typos.dfy(58,9): Error: the parameter named 'low' is already given positionally
 at-attributes-typos.dfy(56,14): Error: Argument to attribute Compile must be a literal
 at-attributes-typos.dfy(55,0): Error: wrong number of arguments (got 2, but attribute 'Compile' expects at most 1: (0: bool))
-at-attributes-typos.dfy(54,0): Error: incorrect argument type for attribute parameter '0' (expected bool, found string)
+at-attributes-typos.dfy(54,9): Error: incorrect argument type for attribute parameter '0' (expected bool, found string)
 at-attributes-typos.dfy(82,0): Error: @Transparent attribute cannot be applied to method
 at-attributes-typos.dfy(80,0): Error: wrong number of arguments (got 1, but attribute 'IsolateAssertions' expects 0)
 at-attributes-typos.dfy(49,0): Error: @Synthesize attribute cannot be applied to module definition
@@ -33,7 +33,7 @@ at-attributes-typos.dfy(40,0): Error: @Verify attribute cannot be applied to mod
 at-attributes-typos.dfy(39,0): Error: @TimeLimitMultiplier attribute cannot be applied to module definition
 at-attributes-typos.dfy(38,0): Error: @TimeLimit attribute cannot be applied to module definition
 at-attributes-typos.dfy(37,0): Error: @ResourceLimit attribute cannot be applied to module definition
-at-attributes-typos.dfy(37,0): Error: incorrect argument type for attribute parameter '0' (expected seq<char>, found int)
+at-attributes-typos.dfy(37,15): Error: incorrect argument type for attribute parameter '0' (expected seq<char>, found int)
 at-attributes-typos.dfy(36,0): Error: @Priority attribute cannot be applied to module definition
 at-attributes-typos.dfy(35,0): Error: @Print attribute cannot be applied to module definition
 at-attributes-typos.dfy(34,0): Error: @VerifyOnly attribute cannot be applied to module definition

Source/IntegrationTests/TestFiles/LitTests/LitTest/autoRevealDependencies/func-depth-fail.dfy.expect

@@ -1,4 +1,4 @@
-func-depth-fail.dfy(12,2): Error: a postcondition could not be proved on this return path
+func-depth-fail.dfy(12,3): Error: a postcondition could not be proved on this return path
 func-depth-fail.dfy(10,10): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 3 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-Resolve.dfy.expect

@@ -54,7 +54,7 @@ AsIs-Resolve.dfy(212,11): Error: type test for type 'int -> real' must be from a
 AsIs-Resolve.dfy(213,11): Error: type test for type 'int -> Odd' must be from an expression assignable to it (got 'int -> nat') (covariant type parameter 1 would require nat <: Odd)
 AsIs-Resolve.dfy(220,11): Error: type test for type 'int ~> real' must be from an expression assignable to it (got 'int ~> nat') (covariant type parameter 1 would require nat <: real)
 AsIs-Resolve.dfy(185,11): Error: type cast to reference type 'C<(int, real)>' must be from an expression assignable to it (got 'M<string>') (non-variant type parameter would require (int, real) = (string, string)) (covariant type parameter 0 would require string <: int)
-AsIs-Resolve.dfy(196,9): Error: incorrect argument type at index 0 for datatype constructor parameter (expected real, found int)
+AsIs-Resolve.dfy(196,14): Error: incorrect argument type at index 0 for datatype constructor parameter (expected real, found int)
 AsIs-Resolve.dfy(229,15): Error: type test for type 'object' must be from an expression assignable to it (got 'T')
 AsIs-Resolve.dfy(230,18): Error: type test for type 'array<object>' must be from an expression assignable to it (got 'array<T>') (nonvariance for type parameter expects object = T)
 AsIs-Resolve.dfy(231,18): Error: type test for type 'array<int>' must be from an expression assignable to it (got 'array<T>') (nonvariance for type parameter expects int = T)

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect

@@ -1,21 +1,21 @@
-AutoReq.dfy(13,2): Error: function precondition could not be proved
+AutoReq.dfy(13,3): Error: function precondition could not be proved
 AutoReq.dfy(5,13): Related location: this proposition could not be proved
-AutoReq.dfy(25,2): Error: function precondition could not be proved
+AutoReq.dfy(25,3): Error: function precondition could not be proved
 AutoReq.dfy(5,13): Related location: this proposition could not be proved
-AutoReq.dfy(38,11): Error: function precondition could not be proved
+AutoReq.dfy(38,12): Error: function precondition could not be proved
 AutoReq.dfy(5,13): Related location: this proposition could not be proved
-AutoReq.dfy(38,11): Error: assertion might not hold
-AutoReq.dfy(31,12): Related location: this proposition could not be proved
+AutoReq.dfy(38,12): Error: assertion might not hold
+AutoReq.dfy(31,13): Related location: this proposition could not be proved
 AutoReq.dfy(7,4): Related location: this proposition could not be proved
-AutoReq.dfy(40,11): Error: function precondition could not be proved
+AutoReq.dfy(40,12): Error: function precondition could not be proved
 AutoReq.dfy(5,13): Related location: this proposition could not be proved
-AutoReq.dfy(40,11): Error: assertion might not hold
-AutoReq.dfy(31,26): Related location: this proposition could not be proved
+AutoReq.dfy(40,12): Error: assertion might not hold
+AutoReq.dfy(31,27): Related location: this proposition could not be proved
 AutoReq.dfy(7,4): Related location: this proposition could not be proved
-AutoReq.dfy(45,11): Error: assertion might not hold
-AutoReq.dfy(31,12): Related location: this proposition could not be proved
+AutoReq.dfy(45,12): Error: assertion might not hold
+AutoReq.dfy(31,13): Related location: this proposition could not be proved
 AutoReq.dfy(7,4): Related location: this proposition could not be proved
-AutoReq.dfy(247,4): Error: function precondition could not be proved
+AutoReq.dfy(247,6): Error: function precondition could not be proved
 AutoReq.dfy(239,13): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 30 verified, 8 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Backticks.dfy.expect

@@ -1,4 +1,4 @@
-Backticks.dfy(38,4): Error: insufficient reads clause to invoke function
+Backticks.dfy(38,5): Error: insufficient reads clause to invoke function
 Backticks.dfy(77,7): Error: call might violate context's modifies clause
 
 Dafny program verifier finished with 12 verified, 2 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BadFunction.dfy.expect

@@ -1,3 +1,3 @@
-BadFunction.dfy(9,2): Error: decreases clause might not decrease
+BadFunction.dfy(9,3): Error: decreases clause might not decrease
 
 Dafny program verifier finished with 1 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BindingGuards.dfy.expect

@@ -304,7 +304,7 @@ method AltSyntax9(x: int, y: int, c: Color)
 datatype Color = Red | Green | Blue
 BindingGuards.dfy(85,10): Error: a postcondition could not be proved on this return path
 BindingGuards.dfy(71,12): Related location: this is the postcondition that could not be proved
-BindingGuards.dfy(134,9): Error: assertion might not hold
+BindingGuards.dfy(134,10): Error: assertion might not hold
 BindingGuards.dfy(6,8): Related location: this proposition could not be proved
 BindingGuards.dfy(139,2): Error: alternative cases fail to cover all possibilities
 BindingGuards.dfy(147,2): Error: alternative cases fail to cover all possibilities

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BindingGuardsResolution.dfy.expect

@@ -164,5 +164,5 @@ BindingGuardsResolution.dfy(132,8): Error: assignment to non-ghost variable is n
 BindingGuardsResolution.dfy(140,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression
 BindingGuardsResolution.dfy(142,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression
 BindingGuardsResolution.dfy(146,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression
-BindingGuardsResolution.dfy(149,37): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword)
+BindingGuardsResolution.dfy(149,38): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword)
 11 resolution/type errors detected in BindingGuardsResolution.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorResolution.dfy.expect

@@ -8,8 +8,8 @@ BitvectorResolution.dfy(38,6): Error: RHS (of type bv67) not assignable to LHS (
 BitvectorResolution.dfy(39,6): Error: RHS (of type bv67) not assignable to LHS (of type int)
 BitvectorResolution.dfy(40,15): Error: type of right argument to << (real) must be an integer-numeric or bitvector type
 BitvectorResolution.dfy(41,15): Error: type of right argument to << (SmallReal) must be an integer-numeric or bitvector type
-BitvectorResolution.dfy(42,25): Error: incorrect argument type for function parameter 'w' (expected nat, found real)
-BitvectorResolution.dfy(43,25): Error: incorrect argument type for function parameter 'w' (expected nat, found SmallReal)
+BitvectorResolution.dfy(42,26): Error: incorrect argument type for function parameter 'w' (expected nat, found real)
+BitvectorResolution.dfy(43,26): Error: incorrect argument type for function parameter 'w' (expected nat, found SmallReal)
 BitvectorResolution.dfy(94,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 BitvectorResolution.dfy(95,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 BitvectorResolution.dfy(96,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorsMore.dfy.expect

@@ -490,7 +490,7 @@ BitvectorsMore.dfy(168,33): Error: when converting shift amount to a bit vector,
 BitvectorsMore.dfy(169,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
 BitvectorsMore.dfy(170,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
 BitvectorsMore.dfy(171,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
-BitvectorsMore.dfy(193,26): Error: rotate amount must not exceed the width of the result (5)
-BitvectorsMore.dfy(194,26): Error: rotate amount must not exceed the width of the result (5)
+BitvectorsMore.dfy(193,36): Error: rotate amount must not exceed the width of the result (5)
+BitvectorsMore.dfy(194,37): Error: rotate amount must not exceed the width of the result (5)
 
 Dafny program verifier finished with 9 verified, 41 errors