cleanup

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -278,7 +278,7 @@ private record ReadsCheckDelayer(ExpressionTranslator etran, Function selfCallsA
  wfOptions = wfOptions.WithLValueContext(false);
  }
 
- var readFrames = (codeContext as MethodOrFunction)?.Reads?.Expressions ?? new();
+ var readFrames = GetContextReadsFrames();
 
  switch (expr) {
  case StaticReceiverExpr stexpr: {
@@ -782,11 +782,7 @@ private record ReadsCheckDelayer(ExpressionTranslator etran, Function selfCallsA
  var receiverSubstMap = readsReceiver.Ins.Zip(e.Args)
  .ToDictionary(fa => fa.First as IVariable, fa => fa.Second);
  var subst = new Substituter(receiverReplacement, receiverSubstMap, e.GetTypeArgumentSubstitutions());
- requiredFrames = (readsReceiver! switch {
- Method m => m.Reads,
- Function f => f.Reads,
- _ => throw new cce.UnreachableException()
- }).Expressions.ConvertAll(subst.SubstFrameExpr);
+ requiredFrames = readsReceiver.Reads.Expressions.ConvertAll(subst.SubstFrameExpr);
  break;
  }
  default:

Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs

@@ -2046,8 +2046,7 @@ public partial class BoogieGenerator {
  if (etran.readsFrame != null) {
  // substitute actual args for parameter in frames for the description expression...
  var requiredFrames = callee.Reads.Expressions.ConvertAll(directSub.SubstFrameExpr);
- var readFrames = (codeContext as MethodOrFunction)?.Reads?.Expressions ?? new();
- var desc = new PODesc.ReadFrameSubset("call", requiredFrames, readFrames);
+ var desc = new PODesc.ReadFrameSubset("call", requiredFrames, GetContextReadsFrames());
 
  // ... but no need to do so for frames passed to CheckFrameSubset
  var readsSubst = new Substituter(null, new Dictionary<IVariable, Expression>(), tySubst);