Ran formatter

dafny-lang · Oct 18, 2024 · 317d20d · 317d20d
1 parent 7c496a2
commit 317d20d
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 17 deletions.
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs
@@ -2372,7 +2372,7 @@ void AddWellformednessCheck(DatatypeCtor ctor) {
       Reset();
     }
 
-    public Bpl.Expr CtorInvocation(IToken tok, DatatypeCtor ctor, ExpressionTranslator etran, 
+    public Bpl.Expr CtorInvocation(IToken tok, DatatypeCtor ctor, ExpressionTranslator etran,
       Variables locals, BoogieStmtListBuilder localTypeAssumptions) {
       Contract.Requires(tok != null);
       Contract.Requires(ctor != null);
@@ -4041,7 +4041,7 @@ Bpl.Expr GetSubrangeCheck(
       return cre;
     }
 
-    public void CheckSubrange(IToken tok, Bpl.Expr bSource, Type sourceType, Type targetType, 
+    public void CheckSubrange(IToken tok, Bpl.Expr bSource, Type sourceType, Type targetType,
       Expression source, BoogieStmtListBuilder builder, string errorMsgPrefix = "") {
       Contract.Requires(tok != null);
       Contract.Requires(bSource != null);
@@ -4870,7 +4870,7 @@ public Expr GetRevealConstant(Function f) {
       this.CreateRevealableConstant(f);
       return this.functionReveals[f];
     }
-  
+
     public static IsAllocType ISALLOC { get { return IsAllocType.ISALLOC; } }
     public static IsAllocType NOALLOC { get { return IsAllocType.NOALLOC; } }
   }

diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs
@@ -787,9 +787,9 @@ private void CommitAllocatedObject(IToken tok, Bpl.IdentifierExpr nw, Bpl.Cmd ex
     // assume $IsHeapAnchor($Heap);
     builder.Add(new Bpl.AssumeCmd(tok, FunctionCall(tok, BuiltinFunction.IsHeapAnchor, null, etran.HeapExpr)));
   }
-  
-public void IntroduceAndAssignExistentialVars(ExistsExpr exists, BoogieStmtListBuilder builder, 
-  BoogieStmtListBuilder builderOutsideIfConstruct, Variables locals, ExpressionTranslator etran, bool isGhost) {
+
+  public void IntroduceAndAssignExistentialVars(ExistsExpr exists, BoogieStmtListBuilder builder,
+    BoogieStmtListBuilder builderOutsideIfConstruct, Variables locals, ExpressionTranslator etran, bool isGhost) {
     Contract.Requires(exists != null);
     Contract.Requires(exists.Range == null);
     Contract.Requires(builder != null);

diff --git a/Source/DafnyCore/Verifier/Statements/IfStatementVerifier.cs b/Source/DafnyCore/Verifier/Statements/IfStatementVerifier.cs
@@ -8,8 +8,8 @@
 namespace DafnyCore.Verifier.Statements;
 
 public class IfStatementVerifier {
-  
-  public static void EmitBoogie(BoogieGenerator generator, IfStmt stmt, BoogieStmtListBuilder builder, 
+
+  public static void EmitBoogie(BoogieGenerator generator, IfStmt stmt, BoogieStmtListBuilder builder,
     Variables locals, BoogieGenerator.ExpressionTranslator etran) {
     Contract.Requires(stmt != null);
     Contract.Requires(builder != null);
@@ -37,7 +37,7 @@ public static void EmitBoogie(BoogieGenerator generator, IfStmt stmt, BoogieStmt
     StmtList elseList;
     IfCmd elseIf = null;
     var elseBuilder = new BoogieStmtListBuilder(generator, generator.Options, builder.Context);
-    if (stmt.IsBindingGuard) {  
+    if (stmt.IsBindingGuard) {
       elseBuilder.Add(generator.TrAssumeCmdWithDependenciesAndExtend(etran, guard.tok, guard, Expr.Not, "if statement binding guard"));
     }
     if (stmt.Els == null) {
@@ -54,8 +54,8 @@ public static void EmitBoogie(BoogieGenerator generator, IfStmt stmt, BoogieStmt
         }
       }
     }
-    builder.Add(new IfCmd(stmt.Tok, 
-      guard == null || stmt.IsBindingGuard ? null : etran.TrExpr(guard), 
+    builder.Add(new IfCmd(stmt.Tok,
+      guard == null || stmt.IsBindingGuard ? null : etran.TrExpr(guard),
       thenList, elseIf, elseList /*, BlockRewriter.AllowSplitQ */));
   }
 }
diff --git a/Source/DafnyCore/Verifier/Statements/MatchStmtVerifier.cs b/Source/DafnyCore/Verifier/Statements/MatchStmtVerifier.cs
@@ -54,7 +54,7 @@ public static void TrMatchStmt(BoogieGenerator generator, MatchStmt stmt, Boogie
       // havoc all bound variables
       b = new BoogieStmtListBuilder(generator, generator.Options, builder.Context);
       var newLocals = new Variables();
-      Expr r = CtorInvocation(generator, mc, stmt.Source.Type, etran, newLocals, b, 
+      Expr r = CtorInvocation(generator, mc, stmt.Source.Type, etran, newLocals, b,
         stmt.IsGhost ? BoogieGenerator.NOALLOC : BoogieGenerator.ISALLOC);
       locals.AddRange(newLocals.Values);
 
@@ -119,13 +119,13 @@ private static void FillMissingCases(IMatch match) {
       Contract.Assert(memberNamesUsed.Count + match.MissingCases.Count == dtd.Ctors.Count);
     }
   }
-  
+
   /// <summary>
   /// If "declareLocals" is "false", then the locals are added only if they are new, that is, if
   /// they don't already exist in "locals".
   /// </summary>
-  private static Expr CtorInvocation(BoogieGenerator generator, MatchCase mc, Type sourceType, 
-    BoogieGenerator.ExpressionTranslator etran, Variables locals, BoogieStmtListBuilder localTypeAssumptions, 
+  private static Expr CtorInvocation(BoogieGenerator generator, MatchCase mc, Type sourceType,
+    BoogieGenerator.ExpressionTranslator etran, Variables locals, BoogieStmtListBuilder localTypeAssumptions,
     IsAllocType isAlloc, bool declareLocals = true) {
     Contract.Requires(mc != null);
     Contract.Requires(sourceType != null);
@@ -158,7 +158,7 @@ private static Expr CtorInvocation(BoogieGenerator generator, MatchCase mc, Type
       if (wh != null) {
         localTypeAssumptions.Add(BoogieGenerator.TrAssumeCmd(p.tok, wh));
       }
-      generator.CheckSubrange(p.tok, new IdentifierExpr(p.tok, local), pFormalType, p.Type, 
+      generator.CheckSubrange(p.tok, new IdentifierExpr(p.tok, local), pFormalType, p.Type,
         new Microsoft.Dafny.IdentifierExpr(p.Tok, p), localTypeAssumptions);
       args.Add(generator.CondApplyBox(mc.tok, new IdentifierExpr(p.tok, local), cce.NonNull(p.Type), mc.Ctor.Formals[i].Type));
     }
@@ -193,7 +193,7 @@ public static void TrMatchExpr(BoogieGenerator boogieGenerator, MatchExpr me, WF
       }
 
       String missingStr = me.Context.FillHole(new IdCtx(missingCtor)).AbstractAllHoles().ToString();
-      b.Add(boogieGenerator.Assert(boogieGenerator.GetToken(me), Expr.False, 
+      b.Add(boogieGenerator.Assert(boogieGenerator.GetToken(me), Expr.False,
         new MatchIsComplete("expression", missingStr), builder.Context));
 
       Expr guard = Expr.Eq(src, r);