Two more structured proof obligation descriptions (#2880)

This adds two more structured proof obligation descriptions and moves
entirely away from `ErrorData` (which was removed in a
boogie-org/boogie#618), allowing Dafny to work with the most recent
Boogie code. These changes should have been included in #1915.

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

Source/DafnyCore/Verifier/Translator.cs

@@ -7214,28 +7214,22 @@ Bpl.PredicateCmd AssertNS(IToken tok, Bpl.Expr condition, PODesc.ProofObligation
       }
     }
 
-    // TODO: update to include structured description
     Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessage, string comment) {
       Contract.Requires(tok != null);
       Contract.Requires(condition != null);
       Contract.Ensures(Contract.Result<Bpl.Ensures>() != null);
 
       Bpl.Ensures ens = new Bpl.Ensures(ForceCheckToken.Unwrap(tok), free, condition, comment);
-      if (errorMessage != null) {
-        ens.ErrorData = errorMessage;
-      }
+      ens.Description = new PODesc.AssertStatement(errorMessage ?? "This is the postcondition that might not hold.");
       return ens;
     }
 
-    // TODO: update to include structured description
     Bpl.Requires Requires(IToken tok, bool free, Bpl.Expr condition, string errorMessage, string comment) {
       Contract.Requires(tok != null);
       Contract.Requires(condition != null);
       Contract.Ensures(Contract.Result<Bpl.Requires>() != null);
       Bpl.Requires req = new Bpl.Requires(ForceCheckToken.Unwrap(tok), free, condition, comment);
-      if (errorMessage != null) {
-        req.ErrorData = errorMessage;
-      }
+      req.Description = new PODesc.AssertStatement(errorMessage ?? "This is the precondition that might not hold.");
       return req;
     }