Allow users to annontate a method as main with {:main} attribute. It’s an error

if more than one method is so annotated. For that method, the usual restrictions
for "main" apply, but it is allowed to take ghost arguments, and it is allowed
to have preconditions.  This lets the programmer add some explicit assumptions
about the outside world, modeled, for example, via ghost parameters.

0 files changed, 0 insertions, 0 deletions