summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2016-03-28 14:51:00 -0700
committerGravatar qunyanm <unknown>2016-03-28 14:51:00 -0700
commit62eb04905d6dcb3ab0b6d7cbf1051c97fec01474 (patch)
tree002242ed44f718fc916ac83643ffdc5682260b3d /Test
parent91cee1c2028f9ad995df863f2a4568d95f4ea1a8 (diff)
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.
Diffstat (limited to 'Test')
0 files changed, 0 insertions, 0 deletions