From 317d20dbcf4f6846545bfc9ab63f716fda36903b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 18 Oct 2024 16:38:17 +0200 Subject: [PATCH] Ran formatter --- Source/DafnyCore/Verifier/BoogieGenerator.cs | 6 +++--- .../Statements/BoogieGenerator.TrStatement.cs | 6 +++--- .../Verifier/Statements/IfStatementVerifier.cs | 10 +++++----- .../Verifier/Statements/MatchStmtVerifier.cs | 12 ++++++------ 4 files changed, 17 insertions(+), 17 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index c4c2d2f8c76..42a98370998 100644 --- 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 index 923f6a8371b..4529330e51b 100644 --- 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 index a0348e49ff5..15616870d41 100644 --- 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 */)); } } \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/Statements/MatchStmtVerifier.cs b/Source/DafnyCore/Verifier/Statements/MatchStmtVerifier.cs index ca09e03ed29..3dfd1d51b0c 100644 --- 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); } } - + /// /// If "declareLocals" is "false", then the locals are added only if they are new, that is, if /// they don't already exist in "locals". /// - 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);