Allow custom error message for assertion failures via @msg annotation

[marcoeilers]

For example,

method test0(x: Ref)
{
   @msg("Custom error message") assert x != null
}

leads to Silicon output

Silicon found 1 error in 2.83s:
  [0] Custom error message

Requested by @tdardinier.

[jcp19]

can this annotation be used in function preconditions too to override the error message if the precondition does not hold?