Regression fix can call (#6041)

<!-- Please remove these Markdown comments before publishing this PR,
since the PR message is often used as the commit description.
We only allow squash merging and GH suggests the PR details as a default
commit message. -->

The PR fixes the this [git
issue](#6038) which describes
how verification fails when repeating the method specification from
trait. This completeness bug which arose because can calls were not
emitted for modifies clauses of methods during their override checks.


<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->

### How has this been tested?
<!-- Tests can be added to
`Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to
`Source/*.Test/…` and run with `dotnet test` -->

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

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/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6038.dfy

@@ -0,0 +1,22 @@
+// RUN: %verify %s &> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T {
+
+  ghost function Modifies(): set<object>
+
+  method Foo()
+    modifies Modifies()
+}
+
+class {:compile false} C extends T {
+
+  const Repr: set<object>
+
+  ghost function Modifies(): set<object> {
+    Repr
+  }
+
+  method Foo()
+    modifies Modifies()
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6038.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors