Documenting compilation errors (dafny-lang#3341)

More work on the error catalog


<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>

Co-authored-by: davidcok <davidcok@github.com>
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
Co-authored-by: stefan-aws <120379523+stefan-aws@users.noreply.github.com>
Co-authored-by: Aaron Tomb <aarontomb@gmail.com>

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -1394,7 +1394,7 @@ public override void Compile(Program program, ConcreteSyntaxTree wrx) {
 
  var wIter = CreateIterator(iter, wr);
  if (iter.Body == null) {
- Error(iter.tok, "Iterator {0} has no body", wIter, iter.FullName);
+ Error(iter.tok, "iterator {0} has no body", wIter, iter.FullName);
  } else {
  TrStmtList(iter.Body.Body, wIter);
  }
@@ -1589,7 +1589,7 @@ public static bool HasMain(Program program, out Method mainMethod) {
  if (member is Method m && member.FullDafnyName == name) {
  mainMethod = m;
  if (!IsPermittedAsMain(program, mainMethod, out string reason)) {
- ReportError(program.Reporter, mainMethod.tok, "The method \"{0}\" is not permitted as a main method ({1}).", null, name, reason);
+ ReportError(program.Reporter, mainMethod.tok, "The method '{0}' is not permitted as a main method ({1}).", null, name, reason);
  mainMethod = null;
  return false;
  } else {
@@ -1618,7 +1618,7 @@ public static bool HasMain(Program program, out Method mainMethod) {
  hasMain = true;
  } else {
  // more than one main in the program
- ReportError(program.Reporter, m.tok, "More than one method is marked \"{{:main}}\". First declaration appeared at {0}.", null,
+ ReportError(program.Reporter, m.tok, "More than one method is marked '{{:main}}'. First declaration appeared at {0}.", null,
  ErrorReporter.TokenToString(mainMethod.tok));
  hasMain = false;
  }
@@ -1629,7 +1629,7 @@ public static bool HasMain(Program program, out Method mainMethod) {
  }
  if (hasMain) {
  if (!IsPermittedAsMain(program, mainMethod, out string reason)) {
- ReportError(program.Reporter, mainMethod.tok, "This method marked \"{{:main}}\" is not permitted as a main method ({0}).", null, reason);
+ ReportError(program.Reporter, mainMethod.tok, "This method marked '{{:main}}' is not permitted as a main method ({0}).", null, reason);
  mainMethod = null;
  return false;
  } else {
@@ -1658,7 +1658,7 @@ public static bool HasMain(Program program, out Method mainMethod) {
  hasMain = true;
  } else {
  // more than one main in the program
- ReportError(program.Reporter, m.tok, "More than one method is declared as \"{0}\". First declaration appeared at {1}.", null,
+ ReportError(program.Reporter, m.tok, "More than one method is declared as '{0}'. First declaration appeared at {1}.", null,
  DefaultNameMain, ErrorReporter.TokenToString(mainMethod.tok));
  hasMain = false;
  }
@@ -1670,7 +1670,7 @@ public static bool HasMain(Program program, out Method mainMethod) {
 
  if (hasMain) {
  if (!IsPermittedAsMain(program, mainMethod, out string reason)) {
- ReportError(program.Reporter, mainMethod.tok, "This method \"Main\" is not permitted as a main method ({0}).", null, reason);
+ ReportError(program.Reporter, mainMethod.tok, "This method 'Main' is not permitted as a main method ({0}).", null, reason);
  return false;
  } else {
  return true;
@@ -3220,7 +3220,7 @@ protected internal void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSy
  var s0 = (AssignStmt)s.S0;
  if (s0.Rhs is HavocRhs) {
  if (DafnyOptions.O.ForbidNondeterminism) {
- Error(s0.Rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr);
+ Error(s0.Rhs.Tok, "nondeterministic assignment forbidden by --enforce-determinism", wr);
  }
  // The forall statement says to havoc a bunch of things. This can be efficiently compiled
  // into doing nothing.
@@ -5113,7 +5113,6 @@ private ConcreteSyntaxTree MaybeInjectSubtypeConstraint(string tmpVarName,
  wr = EmitReturnExpr(wr);
  TrExpr(new LiteralExpr(tok, elseReturnValue), wr, inLetExprBody, wStmts);
  }
-
  wr = thenWriter;
  }
  }
@@ -5138,11 +5137,10 @@ private ConcreteSyntaxTree MaybeInjectSubsetConstraint(IVariable boundVar, Type
  }) {
  if (variable.Type.NormalizeExpandKeepConstraints() is UserDefinedType
  {
- ResolvedClass:
- SubsetTypeDecl
+ ResolvedClass: SubsetTypeDecl
  } normalizedVariableType) {
  wr = MaybeInjectSubsetConstraint(boundVar, normalizedVariableType, collectionElementType,
- inLetExprBody, tok, wr, isReturning, elseReturnValue, true);
+  inLetExprBody, tok, wr, isReturning, elseReturnValue, true);
  }
 
  var bvIdentifier = new IdentifierExpr(tok, boundVar);

Test/allocated1/dafny0/CompilationErrors.dfy.expect

@@ -19,5 +19,5 @@ CompilationErrors.dfy(73,2): Error: a loop without a body cannot be compiled
 CompilationErrors.dfy(83,4): Error: a loop without a body cannot be compiled
 CompilationErrors.dfy(85,4): Error: a loop without a body cannot be compiled
 CompilationErrors.dfy(4,5): Error: Opaque type ('_module.MyType') cannot be compiled; perhaps make it a type synonym or use :extern.
-CompilationErrors.dfy(5,9): Error: Iterator _module.Iter has no body
+CompilationErrors.dfy(5,9): Error: iterator _module.Iter has no body
 CompilationErrors.dfy(12,6): Error: an assume statement without an {:axiom} attribute cannot be compiled

Test/comp/CompileWithArgumentsFail.dfy.expect

@@ -2,4 +2,4 @@
 Dafny program verifier finished with 0 verified, 0 errors
 
 Dafny program verifier did not attempt verification
-CompileWithArgumentsFail.dfy(5,7): Error: This method "Main" is not permitted as a main method (the method's non-ghost argument type should be an seq<string>, got int).
+CompileWithArgumentsFail.dfy(5,7): Error: This method 'Main' is not permitted as a main method (the method's non-ghost argument type should be an seq<string>, got int).

Test/comp/CompileWithArgumentsFail2.dfy.expect

@@ -2,4 +2,4 @@
 Dafny program verifier finished with 0 verified, 0 errors
 
 Dafny program verifier did not attempt verification
-CompileWithArgumentsFail2.dfy(5,7): Error: This method "Main" is not permitted as a main method (the method has two or more non-ghost parameters).
+CompileWithArgumentsFail2.dfy(5,7): Error: This method 'Main' is not permitted as a main method (the method has two or more non-ghost parameters).

Test/comp/compile1verbose/.gitignore

@@ -0,0 +1 @@
+CompileAndThenRun.jar

Test/comp/compile3/.gitignore

@@ -0,0 +1 @@
+JustRun.jar

Test/dafny0/CompilationErrors.dfy.expect

@@ -5,7 +5,7 @@ CompilationErrors.dfy(85,4): Warning: note, this loop has no body (loop frame: i
 
 Dafny program verifier finished with 5 verified, 0 errors
 CompilationErrors.dfy(4,5): Error: Opaque type ('_module.MyType') cannot be compiled; perhaps make it a type synonym or use :extern.
-CompilationErrors.dfy(5,9): Error: Iterator _module.Iter has no body
+CompilationErrors.dfy(5,9): Error: iterator _module.Iter has no body
 CompilationErrors.dfy(12,6): Error: an assume statement without an {:axiom} attribute cannot be compiled
 CompilationErrors.dfy(6,13): Error: Method _module._default.M has no body
 CompilationErrors.dfy(7,7): Error: Method _module._default.P has no body

Test/dafny0/ForbidNondeterminismCompile.dfy.expect

@@ -10,6 +10,6 @@ ForbidNondeterminismCompile.dfy(23,2): Error: case-based if statement forbidden
 ForbidNondeterminismCompile.dfy(32,2): Error: binding if statement forbidden by the --enforce-determinism option
 ForbidNondeterminismCompile.dfy(35,2): Error: nondeterministic loop forbidden by the --enforce-determinism option
 ForbidNondeterminismCompile.dfy(40,2): Error: case-based loop forbidden by the --enforce-determinism option
-ForbidNondeterminismCompile.dfy(48,12): Error: nondeterministic assignment forbidden by the --enforce-determinism option
+ForbidNondeterminismCompile.dfy(48,12): Error: nondeterministic assignment forbidden by --enforce-determinism
 ForbidNondeterminismCompile.dfy(50,2): Error: modify statement without a body forbidden by the --enforce-determinism option
 ForbidNondeterminismCompile.dfy(63,16): Error: nondeterministic assignment forbidden by the --enforce-determinism option

Test/dafny4/Bug62.dfy.expect

@@ -1,4 +1,4 @@
 
 Dafny program verifier finished with 0 verified, 0 errors
-Bug62.dfy(13,9): Error: More than one method is declared as "Main". First declaration appeared at Bug62.dfy(6,9).
-Bug62.dfy(22,16): Error: More than one method is declared as "Main". First declaration appeared at Bug62.dfy(6,9).
+Bug62.dfy(13,9): Error: More than one method is declared as 'Main'. First declaration appeared at Bug62.dfy(6,9).
+Bug62.dfy(22,16): Error: More than one method is declared as 'Main'. First declaration appeared at Bug62.dfy(6,9).

Test/git-issues/git-issue-Main.dfy.expect

@@ -2,19 +2,19 @@
 Dafny program verifier finished with 0 verified, 0 errors
 
 Dafny program verifier did not attempt verification
-git-issue-Main.dfy(16,18): Error: More than one method is declared as "Main". First declaration appeared at git-issue-Main.dfy(10,11).
-git-issue-Main.dfy(20,7): Error: More than one method is declared as "Main". First declaration appeared at git-issue-Main.dfy(10,11).
+git-issue-Main.dfy(16,18): Error: More than one method is declared as 'Main'. First declaration appeared at git-issue-Main.dfy(10,11).
+git-issue-Main.dfy(20,7): Error: More than one method is declared as 'Main'. First declaration appeared at git-issue-Main.dfy(10,11).
 
 Dafny program verifier did not attempt verification
-git-issue-Main.dfy(16,18): Error: More than one method is declared as "Main". First declaration appeared at git-issue-Main.dfy(10,11).
-git-issue-Main.dfy(20,7): Error: More than one method is declared as "Main". First declaration appeared at git-issue-Main.dfy(10,11).
+git-issue-Main.dfy(16,18): Error: More than one method is declared as 'Main'. First declaration appeared at git-issue-Main.dfy(10,11).
+git-issue-Main.dfy(20,7): Error: More than one method is declared as 'Main'. First declaration appeared at git-issue-Main.dfy(10,11).
 
 Dafny program verifier did not attempt verification
-git-issue-Main.dfy(16,18): Error: More than one method is declared as "Main". First declaration appeared at git-issue-Main.dfy(10,11).
-git-issue-Main.dfy(20,7): Error: More than one method is declared as "Main". First declaration appeared at git-issue-Main.dfy(10,11).
+git-issue-Main.dfy(16,18): Error: More than one method is declared as 'Main'. First declaration appeared at git-issue-Main.dfy(10,11).
+git-issue-Main.dfy(20,7): Error: More than one method is declared as 'Main'. First declaration appeared at git-issue-Main.dfy(10,11).
 Wrote textual form of partial target program to git-issue-Main-go/src/git-issue-Main.go
 
 Dafny program verifier did not attempt verification
-git-issue-Main.dfy(16,18): Error: More than one method is declared as "Main". First declaration appeared at git-issue-Main.dfy(10,11).
-git-issue-Main.dfy(20,7): Error: More than one method is declared as "Main". First declaration appeared at git-issue-Main.dfy(10,11).
+git-issue-Main.dfy(16,18): Error: More than one method is declared as 'Main'. First declaration appeared at git-issue-Main.dfy(10,11).
+git-issue-Main.dfy(20,7): Error: More than one method is declared as 'Main'. First declaration appeared at git-issue-Main.dfy(10,11).
 Wrote textual form of partial target program to git-issue-Main-java/git_issue_Main.java

Test/git-issues/git-issue-Main2.dfy.expect

@@ -2,15 +2,15 @@
 Dafny program verifier finished with 0 verified, 0 errors
 
 Dafny program verifier did not attempt verification
-git-issue-Main2.dfy(16,26): Error: More than one method is marked "{:main}". First declaration appeared at git-issue-Main2.dfy(10,19).
+git-issue-Main2.dfy(16,26): Error: More than one method is marked '{:main}'. First declaration appeared at git-issue-Main2.dfy(10,19).
 
 Dafny program verifier did not attempt verification
-git-issue-Main2.dfy(16,26): Error: More than one method is marked "{:main}". First declaration appeared at git-issue-Main2.dfy(10,19).
+git-issue-Main2.dfy(16,26): Error: More than one method is marked '{:main}'. First declaration appeared at git-issue-Main2.dfy(10,19).
 
 Dafny program verifier did not attempt verification
-git-issue-Main2.dfy(16,26): Error: More than one method is marked "{:main}". First declaration appeared at git-issue-Main2.dfy(10,19).
+git-issue-Main2.dfy(16,26): Error: More than one method is marked '{:main}'. First declaration appeared at git-issue-Main2.dfy(10,19).
 Wrote textual form of partial target program to git-issue-Main2-go/src/git-issue-Main2.go
 
 Dafny program verifier did not attempt verification
-git-issue-Main2.dfy(16,26): Error: More than one method is marked "{:main}". First declaration appeared at git-issue-Main2.dfy(10,19).
+git-issue-Main2.dfy(16,26): Error: More than one method is marked '{:main}'. First declaration appeared at git-issue-Main2.dfy(10,19).
 Wrote textual form of partial target program to git-issue-Main2-java/git_issue_Main2.java

Test/git-issues/git-issue-MainE.dfy.expect

@@ -2,16 +2,16 @@
 Dafny program verifier finished with 1 verified, 0 errors
 
 Dafny program verifier did not attempt verification
-git-issue-MainE.dfy(20,9): Error: The method "A.Test" is not permitted as a main method (the method's non-ghost argument type should be an seq<string>, got int).
+git-issue-MainE.dfy(20,9): Error: The method 'A.Test' is not permitted as a main method (the method's non-ghost argument type should be an seq<string>, got int).
 
 Dafny program verifier did not attempt verification
-git-issue-MainE.dfy(23,9): Error: The method "B.Test" is not permitted as a main method (the method has type parameters).
+git-issue-MainE.dfy(23,9): Error: The method 'B.Test' is not permitted as a main method (the method has type parameters).
 
 Dafny program verifier did not attempt verification
 OK-C
 
 Dafny program verifier did not attempt verification
-git-issue-MainE.dfy(30,9): Error: The method "D.Test" is not permitted as a main method (the method is not static and the enclosing class has constructors).
+git-issue-MainE.dfy(30,9): Error: The method 'D.Test' is not permitted as a main method (the method is not static and the enclosing class has constructors).
 
 Dafny program verifier did not attempt verification
 OK-E
@@ -20,27 +20,27 @@ Dafny program verifier did not attempt verification
 OK-G
 
 Dafny program verifier did not attempt verification
-git-issue-MainE.dfy(40,9): Error: The method "H.Test" is not permitted as a main method (the method has non-ghost out parameters).
+git-issue-MainE.dfy(40,9): Error: The method 'H.Test' is not permitted as a main method (the method has non-ghost out parameters).
 
 Dafny program verifier did not attempt verification
 OK-I
 
 Dafny program verifier did not attempt verification
-git-issue-MainE.dfy(46,9): Error: The method "J.Test" is not permitted as a main method (the method has requires clauses).
+git-issue-MainE.dfy(46,9): Error: The method 'J.Test' is not permitted as a main method (the method has requires clauses).
 
 Dafny program verifier did not attempt verification
-git-issue-MainE.dfy(49,9): Error: The method "K.Test" is not permitted as a main method (the method has modifies clauses).
+git-issue-MainE.dfy(49,9): Error: The method 'K.Test' is not permitted as a main method (the method has modifies clauses).
 
 Dafny program verifier did not attempt verification
 Main
 
 Dafny program verifier did not attempt verification
 
 Dafny program verifier did not attempt verification
-git-issue-MainE.dfy(60,9): Error: The method "Tr.Instance" is not permitted as a main method (the method is not static and the enclosing type does not support auto-initialization).
+git-issue-MainE.dfy(60,9): Error: The method 'Tr.Instance' is not permitted as a main method (the method is not static and the enclosing type does not support auto-initialization).
 
 Dafny program verifier did not attempt verification
-git-issue-MainE.dfy(79,16): Error: The method "Opaque.Static" is not permitted as a main method (the enclosing type is an opaque type).
+git-issue-MainE.dfy(79,16): Error: The method 'Opaque.Static' is not permitted as a main method (the enclosing type is an opaque type).
 
 Dafny program verifier did not attempt verification
-git-issue-MainE.dfy(80,9): Error: The method "Opaque.Instance" is not permitted as a main method (the enclosing type is an opaque type).
+git-issue-MainE.dfy(80,9): Error: The method 'Opaque.Instance' is not permitted as a main method (the enclosing type is an opaque type).

docs/DafnyRef/Statements.md

@@ -928,7 +928,7 @@ has the same meaning as
 
 <!-- %no-check -->
 ```dafny
-if exists x :| P { var x :| P; S } else { T }
+if exists x :: P { var x :| P; S } else { T }
 ```
 
 The identifiers bound by ``BindingGuard`` are ghost variables

docs/DafnyRef/Types.md

@@ -715,7 +715,7 @@ type parameter `A` is declared to be restricted to auto-init types,
 the program does not need to explicitly assign any value to the
 out-parameter `a`.
 
-### 8.1.3. Nonempty types: `T(00)`
+### 8.1.3. Nonempty types: `T(00)` {#sec-nonempty-types}
 
 Auto-init types are important in compiled contexts. In ghost contexts, it
 may still be important to know that a type is nonempty. Dafny supports

docs/HowToFAQ/Errors-CommandLine.md

@@ -5,7 +5,8 @@
 
 ## Error: Invalid argument _argument_ to option _option_
 
-```bash <!-- %check-error -->
+<!-- %check-cli -->
+```bash 
 dafny resolve --function-syntax:2 mod.dfy
 ```
 
@@ -17,7 +18,8 @@ in the help document (`dafny -?` or `dafny <command> -h`).
 
 ## Error: Invalid argument _argument_ to option --quantifier-syntax
 
-```bash <!-- %check-error -->
+<!-- %check-cli -->
+```bash 
 dafny resolve --quantifier-syntax:2 null.dfy
 ```