Java Modeling Language (JML) / Things to Do / #62 JMLa \warn, \nowarn etc are still supported

#62 JMLa \warn, \nowarn etc are still supported

Status: open

Owner: Frederic Rioux

Labels: checker (i.e., the jml tool) (12)

Module:

Priority: 7

Updated: 2006-05-19

Created: 2004-06-21

Creator: Patrice Chalin

Private: No

The old JMLa operators \warn, \warn_op, \nowarn,
\nowarn_op are still being accepted. This should not
be the case as they have been superseded by JMLb
operators \*_math.

Discussion

Gary T. Leavens - 2006-05-19

Logged In: YES
user_id=633675

Is this still a problem or has it been fixed?

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Gary T. Leavens - 2006-05-19

labels: 477027 --> checker (i.e., the jml tool)
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

JMLa \warn, \nowarn etc are still supported

Milestone

Searches

Help

#62 JMLa \warn, \nowarn etc are still supported

Discussion