Merge branch 'master' into dependabot/bundler/docs/google-protobuf-3.…

…25.5

Makefile

@@ -1,3 +1,6 @@
+# Run these tasks even if eponymous files or folders exist
+.PHONY: test-dafny exe
+
 DIR=$(realpath $(dir $(firstword $(MAKEFILE_LIST))))
 
 default: exe
@@ -30,6 +33,24 @@ tests:
 test:
 	(cd "${DIR}"; dotnet test Source/IntegrationTests --filter "DisplayName~${name}")
 
+# Run Dafny on an integration test case directly in the folder itself.
+# make test-run name=<part of the path> action="run ..."
+test-dafny:
+	name="$(name)"; \
+	files=$$(cd "${DIR}"/Source/IntegrationTests/TestFiles/LitTests/LitTest; find . -type f -wholename "*$$name*" | grep -E '\.dfy$$'); \
+	count=$$(echo "$$files" | wc -l); \
+  echo "$${files}"; \
+	if [ "$$count" -eq 0 ]; then \
+		echo "No files found matching pattern: $$name"; \
+		exit 1; \
+	else \
+		echo "$$count test files found."; \
+		for file in $$files; do \
+			filedir=$$(dirname "$$file"); \
+			(cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$${filedir}"; "${DIR}"/Binaries/Dafny $(action)  "$$(basename $$file)" ); \
+		done; \
+	fi
+
 tests-verbose:
 	(cd "${DIR}"; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests )
 

Source/DafnyCore.Test/WriterFromOutputHelper.cs

@@ -25,17 +25,29 @@ public override void Write(char value) {
   public override Encoding Encoding => Encoding.Default;
 
   public override void WriteLine(string? value) {
-    output.WriteLine(buffer + value);
+    try {
+      output.WriteLine(buffer + value);
+    } catch {
+      // ignored because of https://github.com/dafny-lang/dafny/issues/5723
+    }
     buffer.Clear();
   }
 
   public override void WriteLine(string format, params object?[] arg) {
-    output.WriteLine(buffer + format, arg);
+    try {
+      output.WriteLine(buffer + format, arg);
+    } catch {
+      // ignored because of https://github.com/dafny-lang/dafny/issues/5723
+    }
     buffer.Clear();
   }
 
   public override void Flush() {
-    output.WriteLine(buffer.ToString());
+    try {
+      output.WriteLine(buffer.ToString());
+    } catch {
+      // ignored because of https://github.com/dafny-lang/dafny/issues/5723
+    }
     base.Flush();
   }
 }

Source/DafnyCore/AST/AstVisitor.cs

@@ -336,7 +336,7 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) {
             VisitUserProvidedType(local.SyntacticType, context);
           }
 
-        } else if (stmt is AssignStmt assignStmt) {
+        } else if (stmt is SingleAssignStmt assignStmt) {
           if (assignStmt.Rhs is TypeRhs typeRhs) {
             if (typeRhs.EType != null) {
               VisitUserProvidedType(typeRhs.EType, context);

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs

@@ -45,7 +45,14 @@ public NestedMatchStmt(Cloner cloner, NestedMatchStmt original) : base(cloner, o
 
   public override IEnumerable<INode> Children => new[] { Source }.Concat<Node>(Cases);
 
-  public override IEnumerable<Statement> SubStatements => Cases.SelectMany(c => c.Body);
+  public override IEnumerable<Statement> SubStatements {
+    get {
+      if (Flattened != null) {
+        return Flattened.SubStatements;
+      }
+      return Cases.SelectMany(c => c.Body);
+    }
+  }
 
   public override IEnumerable<Statement> PreResolveSubStatements {
     get => this.Cases.SelectMany(oneCase => oneCase.Body);

Source/DafnyCore/AST/Expressions/StmtExpr.cs

@@ -63,7 +63,7 @@ public Expression GetSConclusion() {
       return s.Result;
     } else if (S is HideRevealStmt) {
       return CreateBoolLiteral(tok, true);  // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :)
-    } else if (S is UpdateStmt) {
+    } else if (S is AssignStatement) {
       return CreateBoolLiteral(tok, true);  // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :)
     } else {
       Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement