The default output file name is derived from the name of the input file (for example, if the input file is named module.my the output file will be named module.defs). The -o option overrides this behavior with the specified output file name; if you specify a dash ``-'' with the -o option, the standard output is used instead of a file.
Normally, mosy prints the name of each object, identifier, or type as it works. The -s option disables this behavior.
mosy discards the enumerations associated with ints (although it does perform range checking on them).
mosy does not perform range checking on size constraints associated with ints.
RFC 1155, RFC 1212