org.jmlspecs.checker
Class JmlMessages

java.lang.Object
  org.jmlspecs.checker.JmlMessages

public class JmlMessages

extends Object

Field Summary
static MessageDescription	ADMISSIBILITY_METHOD_CALL_NOT_SUPPORTED
static MessageDescription	ADMISSIBILITY_OBJECT_CREATION_NOT_SUPPORTED
static MessageDescription	ADMISSIBILITY_STATICS_NOT_SUPPORTED
static MessageDescription	AMBIGUOUS_CALLABLE_METHOD
static MessageDescription	ARITHMETIC_MODE_CONFLICT
static MessageDescription	ARRAY_NULLITY_DECLARATION_MISMATCH
static MessageDescription	ASSERTIONS_FOR_MORE_THAN_ONE_VAR
static MessageDescription	ASSIGNABLE_CHECKING
static MessageDescription	AXIOM_MODIFIERS
static MessageDescription	BAD_ABRUPT_SPEC_BODY
static MessageDescription	BAD_EXCEPTIONAL_SPEC_BODY
static MessageDescription	BAD_INITIALIZER_MODIFIERS
static MessageDescription	BAD_NORMAL_SPEC_BODY
static MessageDescription	BAD_PARAM_MOD_ORDER
static MessageDescription	BAD_PRIVACY_MODIFIER
static MessageDescription	BAD_SIMPLE_SPEC_BODY
static MessageDescription	BAD_SIMPLE_SPEC_STATEMENT_BODY
static MessageDescription	BAD_SPEC_BODY_ORDER
static MessageDescription	BAD_STORE_REF_KEYWORD
static MessageDescription	BAD_TYPE_IN_DECREASING_STATEMENT
static MessageDescription	BAD_TYPE_IN_DURATION_CLAUSE
static MessageDescription	BAD_TYPE_IN_MEASURED_CLAUSE
static MessageDescription	BAD_TYPE_IN_SIGNALS
static MessageDescription	BAD_TYPE_IN_SIGNALS_ONLY
static MessageDescription	BAD_TYPE_IN_WORKING_SPACE_CLAUSE
static MessageDescription	CLASS_AFTER_MEMBER
static MessageDescription	CLASS_FLAGS
static MessageDescription	CLASS_LEVEL_NULLABLE_NON_NULL_TOGETHER
static MessageDescription	CLASS_NAME_REFINING_FILENAME
static MessageDescription	CLASS_NOT_DEFINED
static MessageDescription	DATA_GROUP_LOCALITY
static MessageDescription	DATA_GROUP_NOT_MODEL
static MessageDescription	DATA_GROUP_VISIBILITY
static MessageDescription	DIFFERENT_REFINING_ACCESS
static MessageDescription	DIFFERENT_REFINING_FIELD_TYPE
static MessageDescription	DUPLICATE_SAME_PREDICATE
static MessageDescription	DURATION_MUST_CONTAIN_METHOD_CALL
static MessageDescription	DURATION_NOT_ALLOWED
static MessageDescription	EQUIVALENCE_TYPE
static MessageDescription	EXTENDING_SPEC_MODIFIERS
static MessageDescription	EXTRANEOUS_ALSO
static MessageDescription	FIELD2_VISIBILITY
static MessageDescription	FIELD_FLAGS
static MessageDescription	FIELD_INIT_NOT_IN_JAVA_FILE
static MessageDescription	FIELD_VISIBILITY
static MessageDescription	FIELD_WITH_MORE_THAN_ONE_INITIALIZER
static MessageDescription	FLAG_GHOST_AND_SPEC_PUBLIC
static MessageDescription	FLAG_INSTANCE_AND_STATIC
static MessageDescription	FLAG_INSTANCE_WITHOUT_MODEL
static MessageDescription	FLAG_MODEL_AND_FINAL
static MessageDescription	FLAG_MODEL_AND_GHOST
static MessageDescription	FLAG_MODEL_AND_SPEC_PUBLIC
static MessageDescription	FLAG_SPEC_PROTECTED
static MessageDescription	FLAG_SPEC_PUBLIC
static MessageDescription	FLAG_SPEC_PUBLIC_AND_PROTECTED
static MessageDescription	FLAG_SPEC_PUBLIC_AND_PUBLIC
static MessageDescription	FRESH_NOT_ALLOWED
static MessageDescription	GENERIC_SPEC_CASE_MODIFIERS
static MessageDescription	GHOST_FIELD_ACCESS
static MessageDescription	ILL_FORMED_SET_COMPREHENSION
static MessageDescription	ILLEGAL_CODE_MODIFIER
static MessageDescription	ILLEGAL_MODEL_PROG_STATEMENT
static MessageDescription	ILLEGAL_SAME_PREDICATE
static MessageDescription	IMPLICIT_NULLITY
static MessageDescription	INVALID_EXCLUDEFILES_PATTERN_SYNTAX
static MessageDescription	INVALID_FIELD_NAME_IN_MAPS_CLAUSE
static MessageDescription	INVALID_FILE_SUFFIX
static MessageDescription	INVALID_LOCAL_MODIFIER
static MessageDescription	INVALID_MAPS_CLAUSE
static MessageDescription	INVALID_MODEL_FIELD_IN_ASSIGNABLE
static MessageDescription	INVALID_PARAM_MODIFIER
static MessageDescription	INVALID_REFINE_FILE_SUFFIX
static MessageDescription	INVALID_REFINING_MODIFIER
static MessageDescription	INVALID_REFINING_PARAMETER_NAME
static MessageDescription	INVALID_REFINING_PARAMETER_NULLITY
static MessageDescription	INVALID_SELF_REFINEMENT
static MessageDescription	INVARIANT_FALSE
static MessageDescription	JAVADOC_FAILURE
static MessageDescription	JML_DECLARATION_FLAGS
static MessageDescription	JML_FLAGS_MULTIPLE_PRIVACY
static MessageDescription	JML_FLAGS_STATIC_AND_INSTANCE
static MessageDescription	LABEL_UNKNOWN
static MessageDescription	LHS_OF_ASSIGN_STATEMENT
static MessageDescription	LHS_OF_SET_STATEMENT
static MessageDescription	LIGHT_WEIGHTED_EXAMPLE_SPEC
static MessageDescription	LOOP_STMT_EXPECTED
static MessageDescription	METHOD2_VISIBILITY
static MessageDescription	METHOD_BODY_NOT_IN_JAVA_FILE
static MessageDescription	METHOD_FLAGS
static MessageDescription	METHOD_MAY_NOT_PURE
static MessageDescription	METHOD_MODIFIER_MISMATCH
static MessageDescription	METHOD_NON_NULL_IN_SUPER
static MessageDescription	METHOD_NOT_DEFINED
static MessageDescription	METHOD_NOT_PURE
static MessageDescription	METHOD_SPEC_INCONSISTENT
static MessageDescription	METHOD_SPEC_PRIVACY
static MessageDescription	METHOD_VISIBILITY
static MessageDescription	MISPLACED_DOT_STAR
static MessageDescription	MISSING_ALSO
static MessageDescription	MISSING_REFINING_ALSO
static MessageDescription	MISSING_REPRESENTS
static MessageDescription	MODEL_FIELD_ACCESS
static MessageDescription	MODEL_FIELD_WITH_INITIALIZER
static MessageDescription	MODEL_IN_PREFIX_EXPRESSION
static MessageDescription	MODEL_LHS_IN_ASSIGNMENT
static MessageDescription	MODEL_METHOD_WITH_MORE_THAN_ONE_BODY
static MessageDescription	MONITORED_FOR_STATIC
static MessageDescription	MULTIPLE_PRIVACY_MODIFIER
static MessageDescription	MULTIPLE_VAR_DECL
static MessageDescription	NESTED_ANNOTATION
static MessageDescription	NESTED_SAME_PREDICATE
static MessageDescription	NO_ASSIGNABLE
static MessageDescription	NO_ASSIGNMENT_EXPRESSION
static MessageDescription	NO_POSTFIX_EXPRESSION
static MessageDescription	NO_PREFIX_EXPRESSION
static MessageDescription	NON_MATCHING_PARAMETER_NAME
static MessageDescription	NON_MODEL_FIELD_NOT_DEFINED
static MessageDescription	NON_MODEL_METHOD_NOT_DEFINED
static MessageDescription	NON_PRIVATE_HELPER
static MessageDescription	NOT_ADMISSIBLE
static MessageDescription	NOT_ADMISSIBLE_REP_FIELD_PRIVATE
static MessageDescription	NOT_ADMISSIBLE_REP_METHOD_PRIVATE
static MessageDescription	NOT_ASSIGNABLE_FIELD
static MessageDescription	NOT_ASSIGNED_NOT_ALLOWED
static MessageDescription	NOT_BOOLEAN
static MessageDescription	NOT_BOOLEAN_IN_ASSUME
static MessageDescription	NOT_BOOLEAN_IN_QUANTIFIED
static MessageDescription	NOT_CALLABLE_METHOD
static MessageDescription	NOT_CLASS_TYPE
static MessageDescription	NOT_INTEGRAL_EXPRESSION
static MessageDescription	NOT_JMLTYPE_SET_MEMBER_TYPE
static MessageDescription	NOT_MODIFIED_NOT_ALLOWED
static MessageDescription	NOT_NON_ARRAY_REFERENCE_TYPE_IN_FIELDS_OF
static MessageDescription	NOT_NON_ARRAY_REFERENCE_TYPE_IN_METHOD_NAME
static MessageDescription	NOT_NON_ARRAY_REFERENCE_TYPE_IN_REACH
static MessageDescription	NOT_NUMERIC_IN_QUANTIFIED
static MessageDescription	NOT_REFERENCE_EXPRESSION
static MessageDescription	NOT_REFERENCE_EXPRESSION_IN_FIELDS_OF
static MessageDescription	NOT_REFERENCE_EXPRESSION_IN_REACH
static MessageDescription	NOT_REFERENCE_SET_MEMBER_TYPE
static MessageDescription	NOT_REFERENCE_TYPE_IN_FIELDS_OF
static MessageDescription	NOT_REFERENCE_TYPE_IN_INVARIANT_FOR
static MessageDescription	NOT_REFERENCE_TYPE_IN_REACH
static MessageDescription	NOT_SUBTYPE_OF_IN_FIELDS_OF
static MessageDescription	NOT_TYPE_IN_ELEMTYPE
static MessageDescription	NULLABLE_NON_NULL_TOGETHER
static MessageDescription	NULLITY_MODIFIERS_FOR_NON_REF_TYPE
static MessageDescription	OLD_NOT_ALLOWED
static MessageDescription	ONLY_ACCESSED_NOT_ALLOWED
static MessageDescription	ONLY_ASSIGNED_NOT_ALLOWED
static MessageDescription	ONLY_CALLED_NOT_ALLOWED
static MessageDescription	ONLY_CAPTURED_NOT_ALLOWED
static MessageDescription	PARAMETER_NULLITY_MISMATCH
static MessageDescription	PARSING
static MessageDescription	PRE_NOT_ALLOWED
static MessageDescription	PURE_AND_ASSIGNABLE
static MessageDescription	PURE_AND_CALLS_NON_PURE
static MessageDescription	RECEIVER_IN_ASSIGNABLE
static MessageDescription	REDUNDANT_REPRESENTS
static MessageDescription	REDUNDANT_SPEC_MODIFIERS
static MessageDescription	REFINE_FILE_CYCLE
static MessageDescription	REFINE_FILE_NOT_FOUND
static MessageDescription	REFINING_METHOD_RETURN_DIFFERENT
static MessageDescription	REFINING_METHOD_THROWS_DIFFERENT
static MessageDescription	REPRESENTS_LOCALITY
static MessageDescription	REPRESENTS_NOT_MODEL
static MessageDescription	REPRESENTS_STATIC_FIELD
static MessageDescription	REPRESENTS_STATIC_LOCALITY
static MessageDescription	REPRESENTS_TYPE_MISMATCH
static MessageDescription	RESULT_NOT_ALLOWED
static MessageDescription	RESULT_VOID
static MessageDescription	RHS_OF_SET_STATEMENT
static MessageDescription	SET_COMPREHENSION_TYPE
static MessageDescription	SET_STATEMENT
static MessageDescription	SPACE_NOT_ALLOWED
static MessageDescription	SPEC_DISCARDED_BLOCKEND
static MessageDescription	SPEC_DISCARDED_SEMI
static MessageDescription	SUBCLASSING_CONTRACT
static MessageDescription	SUBTYPE_OF_TYPE
static MessageDescription	SUPER_NOT_ALLOWED
static MessageDescription	SYNCHRONIZED_PURE
static MessageDescription	THIS_NOT_ALLOWED
static MessageDescription	TYPE2_VISIBILITY
static MessageDescription	TYPE_IN_FRESH
static MessageDescription	TYPE_IN_LABELED_EXPRESSION
static MessageDescription	TYPE_IN_NONNULLELEMENTS
static MessageDescription	TYPE_IN_SPACE
static MessageDescription	TYPE_NAME_IN_TYPE_OF_EXPRESSION
static MessageDescription	TYPE_UNKNOWN
static MessageDescription	TYPE_VISIBILITY
static MessageDescription	TYPECHECKING
static MessageDescription	UNBALANCED_PAREN
static MessageDescription	UNCAUGHT_EXCEPTION_IN_SIGNALS
static MessageDescription	UNEXPECTED_NULLITY_ANNOTATION
static MessageDescription	UNINITIALIZED_OLD_VAR
static MessageDescription	UNSAFE_ARITHMETIC_OPERATION
static MessageDescription	UNUSED_METHOD_SPEC
static MessageDescription	WORKING_SPACE_MUST_CONTAIN_METHOD_CALL
static MessageDescription	WORKING_SPACE_NOT_ALLOWED

 

Constructor Summary

JmlMessages()

 

Method Summary

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

UNBALANCED_PAREN

public static final MessageDescription UNBALANCED_PAREN

LOOP_STMT_EXPECTED

public static final MessageDescription LOOP_STMT_EXPECTED

SET_STATEMENT

public static final MessageDescription SET_STATEMENT

LHS_OF_ASSIGN_STATEMENT

public static final MessageDescription LHS_OF_ASSIGN_STATEMENT

LHS_OF_SET_STATEMENT

public static final MessageDescription LHS_OF_SET_STATEMENT

RHS_OF_SET_STATEMENT

public static final MessageDescription RHS_OF_SET_STATEMENT

MODEL_LHS_IN_ASSIGNMENT

public static final MessageDescription MODEL_LHS_IN_ASSIGNMENT

MODEL_IN_PREFIX_EXPRESSION

public static final MessageDescription MODEL_IN_PREFIX_EXPRESSION

REFINE_FILE_NOT_FOUND

public static final MessageDescription REFINE_FILE_NOT_FOUND

CLASS_AFTER_MEMBER

public static final MessageDescription CLASS_AFTER_MEMBER

UNUSED_METHOD_SPEC

public static final MessageDescription UNUSED_METHOD_SPEC

NESTED_ANNOTATION

public static final MessageDescription NESTED_ANNOTATION

ILLEGAL_MODEL_PROG_STATEMENT

public static final MessageDescription ILLEGAL_MODEL_PROG_STATEMENT

BAD_INITIALIZER_MODIFIERS

public static final MessageDescription BAD_INITIALIZER_MODIFIERS

AXIOM_MODIFIERS

public static final MessageDescription AXIOM_MODIFIERS

EXTENDING_SPEC_MODIFIERS

public static final MessageDescription EXTENDING_SPEC_MODIFIERS

INVALID_LOCAL_MODIFIER

public static final MessageDescription INVALID_LOCAL_MODIFIER

INVALID_PARAM_MODIFIER

public static final MessageDescription INVALID_PARAM_MODIFIER

METHOD_MODIFIER_MISMATCH

public static final MessageDescription METHOD_MODIFIER_MISMATCH

GENERIC_SPEC_CASE_MODIFIERS

public static final MessageDescription GENERIC_SPEC_CASE_MODIFIERS

REDUNDANT_SPEC_MODIFIERS

public static final MessageDescription REDUNDANT_SPEC_MODIFIERS

BAD_PRIVACY_MODIFIER

public static final MessageDescription BAD_PRIVACY_MODIFIER

MULTIPLE_PRIVACY_MODIFIER

public static final MessageDescription MULTIPLE_PRIVACY_MODIFIER

MISPLACED_DOT_STAR

public static final MessageDescription MISPLACED_DOT_STAR

BAD_STORE_REF_KEYWORD

public static final MessageDescription BAD_STORE_REF_KEYWORD

BAD_SIMPLE_SPEC_BODY

public static final MessageDescription BAD_SIMPLE_SPEC_BODY

BAD_NORMAL_SPEC_BODY

public static final MessageDescription BAD_NORMAL_SPEC_BODY

BAD_EXCEPTIONAL_SPEC_BODY

public static final MessageDescription BAD_EXCEPTIONAL_SPEC_BODY

BAD_SIMPLE_SPEC_STATEMENT_BODY

public static final MessageDescription BAD_SIMPLE_SPEC_STATEMENT_BODY

BAD_ABRUPT_SPEC_BODY

public static final MessageDescription BAD_ABRUPT_SPEC_BODY

LIGHT_WEIGHTED_EXAMPLE_SPEC

public static final MessageDescription LIGHT_WEIGHTED_EXAMPLE_SPEC

ARITHMETIC_MODE_CONFLICT

public static final MessageDescription ARITHMETIC_MODE_CONFLICT

NO_ASSIGNMENT_EXPRESSION

public static final MessageDescription NO_ASSIGNMENT_EXPRESSION

NO_PREFIX_EXPRESSION

public static final MessageDescription NO_PREFIX_EXPRESSION

NO_POSTFIX_EXPRESSION

public static final MessageDescription NO_POSTFIX_EXPRESSION

FIELD_VISIBILITY

public static final MessageDescription FIELD_VISIBILITY

FIELD2_VISIBILITY

public static final MessageDescription FIELD2_VISIBILITY

METHOD_VISIBILITY

public static final MessageDescription METHOD_VISIBILITY

METHOD2_VISIBILITY

public static final MessageDescription METHOD2_VISIBILITY

TYPE_VISIBILITY

public static final MessageDescription TYPE_VISIBILITY

TYPE2_VISIBILITY

public static final MessageDescription TYPE2_VISIBILITY

METHOD_SPEC_PRIVACY

public static final MessageDescription METHOD_SPEC_PRIVACY

REPRESENTS_STATIC_LOCALITY

public static final MessageDescription REPRESENTS_STATIC_LOCALITY

REPRESENTS_LOCALITY

public static final MessageDescription REPRESENTS_LOCALITY

REPRESENTS_STATIC_FIELD

public static final MessageDescription REPRESENTS_STATIC_FIELD

REPRESENTS_TYPE_MISMATCH

public static final MessageDescription REPRESENTS_TYPE_MISMATCH

REPRESENTS_NOT_MODEL

public static final MessageDescription REPRESENTS_NOT_MODEL

REDUNDANT_REPRESENTS

public static final MessageDescription REDUNDANT_REPRESENTS

DATA_GROUP_VISIBILITY

public static final MessageDescription DATA_GROUP_VISIBILITY

DATA_GROUP_LOCALITY

public static final MessageDescription DATA_GROUP_LOCALITY

DATA_GROUP_NOT_MODEL

public static final MessageDescription DATA_GROUP_NOT_MODEL

CLASS_FLAGS

public static final MessageDescription CLASS_FLAGS

METHOD_FLAGS

public static final MessageDescription METHOD_FLAGS

FIELD_FLAGS

public static final MessageDescription FIELD_FLAGS

MONITORED_FOR_STATIC

public static final MessageDescription MONITORED_FOR_STATIC

FLAG_INSTANCE_AND_STATIC

public static final MessageDescription FLAG_INSTANCE_AND_STATIC

FLAG_SPEC_PUBLIC

public static final MessageDescription FLAG_SPEC_PUBLIC

FLAG_SPEC_PROTECTED

public static final MessageDescription FLAG_SPEC_PROTECTED

FLAG_SPEC_PUBLIC_AND_PROTECTED

public static final MessageDescription FLAG_SPEC_PUBLIC_AND_PROTECTED

FLAG_MODEL_AND_SPEC_PUBLIC

public static final MessageDescription FLAG_MODEL_AND_SPEC_PUBLIC

FLAG_INSTANCE_WITHOUT_MODEL

public static final MessageDescription FLAG_INSTANCE_WITHOUT_MODEL

FLAG_GHOST_AND_SPEC_PUBLIC

public static final MessageDescription FLAG_GHOST_AND_SPEC_PUBLIC

FLAG_MODEL_AND_GHOST

public static final MessageDescription FLAG_MODEL_AND_GHOST

FLAG_MODEL_AND_FINAL

public static final MessageDescription FLAG_MODEL_AND_FINAL

FLAG_SPEC_PUBLIC_AND_PUBLIC

public static final MessageDescription FLAG_SPEC_PUBLIC_AND_PUBLIC

JML_DECLARATION_FLAGS

public static final MessageDescription JML_DECLARATION_FLAGS

JML_FLAGS_STATIC_AND_INSTANCE

public static final MessageDescription JML_FLAGS_STATIC_AND_INSTANCE

JML_FLAGS_MULTIPLE_PRIVACY

public static final MessageDescription JML_FLAGS_MULTIPLE_PRIVACY

NON_PRIVATE_HELPER

public static final MessageDescription NON_PRIVATE_HELPER

NULLITY_MODIFIERS_FOR_NON_REF_TYPE

public static final MessageDescription NULLITY_MODIFIERS_FOR_NON_REF_TYPE

DIFFERENT_REFINING_FIELD_TYPE

public static final MessageDescription DIFFERENT_REFINING_FIELD_TYPE

DIFFERENT_REFINING_ACCESS

public static final MessageDescription DIFFERENT_REFINING_ACCESS

INVALID_REFINING_MODIFIER

public static final MessageDescription INVALID_REFINING_MODIFIER

NON_MODEL_FIELD_NOT_DEFINED

public static final MessageDescription NON_MODEL_FIELD_NOT_DEFINED

NON_MODEL_METHOD_NOT_DEFINED

public static final MessageDescription NON_MODEL_METHOD_NOT_DEFINED

REFINING_METHOD_RETURN_DIFFERENT

public static final MessageDescription REFINING_METHOD_RETURN_DIFFERENT

REFINING_METHOD_THROWS_DIFFERENT

public static final MessageDescription REFINING_METHOD_THROWS_DIFFERENT

NOT_BOOLEAN_IN_ASSUME

public static final MessageDescription NOT_BOOLEAN_IN_ASSUME

SUBTYPE_OF_TYPE

public static final MessageDescription SUBTYPE_OF_TYPE

TYPE_NAME_IN_TYPE_OF_EXPRESSION

public static final MessageDescription TYPE_NAME_IN_TYPE_OF_EXPRESSION

NOT_NON_ARRAY_REFERENCE_TYPE_IN_METHOD_NAME

public static final MessageDescription NOT_NON_ARRAY_REFERENCE_TYPE_IN_METHOD_NAME

NOT_INTEGRAL_EXPRESSION

public static final MessageDescription NOT_INTEGRAL_EXPRESSION

NOT_REFERENCE_EXPRESSION

public static final MessageDescription NOT_REFERENCE_EXPRESSION

NOT_REFERENCE_EXPRESSION_IN_FIELDS_OF

public static final MessageDescription NOT_REFERENCE_EXPRESSION_IN_FIELDS_OF

NOT_REFERENCE_TYPE_IN_FIELDS_OF

public static final MessageDescription NOT_REFERENCE_TYPE_IN_FIELDS_OF

NOT_NON_ARRAY_REFERENCE_TYPE_IN_FIELDS_OF

public static final MessageDescription NOT_NON_ARRAY_REFERENCE_TYPE_IN_FIELDS_OF

NOT_SUBTYPE_OF_IN_FIELDS_OF

public static final MessageDescription NOT_SUBTYPE_OF_IN_FIELDS_OF

BAD_TYPE_IN_MEASURED_CLAUSE

public static final MessageDescription BAD_TYPE_IN_MEASURED_CLAUSE

BAD_TYPE_IN_DECREASING_STATEMENT

public static final MessageDescription BAD_TYPE_IN_DECREASING_STATEMENT

BAD_TYPE_IN_WORKING_SPACE_CLAUSE

public static final MessageDescription BAD_TYPE_IN_WORKING_SPACE_CLAUSE

BAD_TYPE_IN_DURATION_CLAUSE

public static final MessageDescription BAD_TYPE_IN_DURATION_CLAUSE

BAD_TYPE_IN_SIGNALS_ONLY

public static final MessageDescription BAD_TYPE_IN_SIGNALS_ONLY

BAD_TYPE_IN_SIGNALS

public static final MessageDescription BAD_TYPE_IN_SIGNALS

UNCAUGHT_EXCEPTION_IN_SIGNALS

public static final MessageDescription UNCAUGHT_EXCEPTION_IN_SIGNALS

UNINITIALIZED_OLD_VAR

public static final MessageDescription UNINITIALIZED_OLD_VAR

NOT_REFERENCE_EXPRESSION_IN_REACH

public static final MessageDescription NOT_REFERENCE_EXPRESSION_IN_REACH

NOT_REFERENCE_TYPE_IN_REACH

public static final MessageDescription NOT_REFERENCE_TYPE_IN_REACH

NOT_NON_ARRAY_REFERENCE_TYPE_IN_REACH

public static final MessageDescription NOT_NON_ARRAY_REFERENCE_TYPE_IN_REACH

DUPLICATE_SAME_PREDICATE

public static final MessageDescription DUPLICATE_SAME_PREDICATE

NESTED_SAME_PREDICATE

public static final MessageDescription NESTED_SAME_PREDICATE

ILLEGAL_SAME_PREDICATE

public static final MessageDescription ILLEGAL_SAME_PREDICATE

ILLEGAL_CODE_MODIFIER

public static final MessageDescription ILLEGAL_CODE_MODIFIER

NOT_BOOLEAN

public static final MessageDescription NOT_BOOLEAN

MULTIPLE_VAR_DECL

public static final MessageDescription MULTIPLE_VAR_DECL

NOT_BOOLEAN_IN_QUANTIFIED

public static final MessageDescription NOT_BOOLEAN_IN_QUANTIFIED

NOT_NUMERIC_IN_QUANTIFIED

public static final MessageDescription NOT_NUMERIC_IN_QUANTIFIED

SET_COMPREHENSION_TYPE

public static final MessageDescription SET_COMPREHENSION_TYPE

ILL_FORMED_SET_COMPREHENSION

public static final MessageDescription ILL_FORMED_SET_COMPREHENSION

NOT_REFERENCE_SET_MEMBER_TYPE

public static final MessageDescription NOT_REFERENCE_SET_MEMBER_TYPE

NOT_JMLTYPE_SET_MEMBER_TYPE

public static final MessageDescription NOT_JMLTYPE_SET_MEMBER_TYPE

RESULT_VOID

public static final MessageDescription RESULT_VOID

TYPE_IN_NONNULLELEMENTS

public static final MessageDescription TYPE_IN_NONNULLELEMENTS

NOT_TYPE_IN_ELEMTYPE

public static final MessageDescription NOT_TYPE_IN_ELEMTYPE

NOT_REFERENCE_TYPE_IN_INVARIANT_FOR

public static final MessageDescription NOT_REFERENCE_TYPE_IN_INVARIANT_FOR

NOT_CLASS_TYPE

public static final MessageDescription NOT_CLASS_TYPE

TYPE_UNKNOWN

public static final MessageDescription TYPE_UNKNOWN

FRESH_NOT_ALLOWED

public static final MessageDescription FRESH_NOT_ALLOWED

TYPE_IN_FRESH

public static final MessageDescription TYPE_IN_FRESH

TYPE_IN_SPACE

public static final MessageDescription TYPE_IN_SPACE

TYPE_IN_LABELED_EXPRESSION

public static final MessageDescription TYPE_IN_LABELED_EXPRESSION

LABEL_UNKNOWN

public static final MessageDescription LABEL_UNKNOWN

NOT_MODIFIED_NOT_ALLOWED

public static final MessageDescription NOT_MODIFIED_NOT_ALLOWED

NOT_ASSIGNED_NOT_ALLOWED

public static final MessageDescription NOT_ASSIGNED_NOT_ALLOWED

ONLY_ACCESSED_NOT_ALLOWED

public static final MessageDescription ONLY_ACCESSED_NOT_ALLOWED

ONLY_CALLED_NOT_ALLOWED

public static final MessageDescription ONLY_CALLED_NOT_ALLOWED

ONLY_CAPTURED_NOT_ALLOWED

public static final MessageDescription ONLY_CAPTURED_NOT_ALLOWED

ONLY_ASSIGNED_NOT_ALLOWED

public static final MessageDescription ONLY_ASSIGNED_NOT_ALLOWED

OLD_NOT_ALLOWED

public static final MessageDescription OLD_NOT_ALLOWED

PRE_NOT_ALLOWED

public static final MessageDescription PRE_NOT_ALLOWED

SPACE_NOT_ALLOWED

public static final MessageDescription SPACE_NOT_ALLOWED

WORKING_SPACE_NOT_ALLOWED

public static final MessageDescription WORKING_SPACE_NOT_ALLOWED

DURATION_NOT_ALLOWED

public static final MessageDescription DURATION_NOT_ALLOWED

INVALID_FIELD_NAME_IN_MAPS_CLAUSE

public static final MessageDescription INVALID_FIELD_NAME_IN_MAPS_CLAUSE

WORKING_SPACE_MUST_CONTAIN_METHOD_CALL

public static final MessageDescription WORKING_SPACE_MUST_CONTAIN_METHOD_CALL

DURATION_MUST_CONTAIN_METHOD_CALL

public static final MessageDescription DURATION_MUST_CONTAIN_METHOD_CALL

RESULT_NOT_ALLOWED

public static final MessageDescription RESULT_NOT_ALLOWED

THIS_NOT_ALLOWED

public static final MessageDescription THIS_NOT_ALLOWED

SUPER_NOT_ALLOWED

public static final MessageDescription SUPER_NOT_ALLOWED

EQUIVALENCE_TYPE

public static final MessageDescription EQUIVALENCE_TYPE

INVALID_FILE_SUFFIX

public static final MessageDescription INVALID_FILE_SUFFIX

INVALID_EXCLUDEFILES_PATTERN_SYNTAX

public static final MessageDescription INVALID_EXCLUDEFILES_PATTERN_SYNTAX

INVALID_SELF_REFINEMENT

public static final MessageDescription INVALID_SELF_REFINEMENT

INVALID_REFINE_FILE_SUFFIX

public static final MessageDescription INVALID_REFINE_FILE_SUFFIX

REFINE_FILE_CYCLE

public static final MessageDescription REFINE_FILE_CYCLE

CLASS_NAME_REFINING_FILENAME

public static final MessageDescription CLASS_NAME_REFINING_FILENAME

INVALID_REFINING_PARAMETER_NAME

public static final MessageDescription INVALID_REFINING_PARAMETER_NAME

INVALID_REFINING_PARAMETER_NULLITY

public static final MessageDescription INVALID_REFINING_PARAMETER_NULLITY

METHOD_BODY_NOT_IN_JAVA_FILE

public static final MessageDescription METHOD_BODY_NOT_IN_JAVA_FILE

MODEL_METHOD_WITH_MORE_THAN_ONE_BODY

public static final MessageDescription MODEL_METHOD_WITH_MORE_THAN_ONE_BODY

FIELD_WITH_MORE_THAN_ONE_INITIALIZER

public static final MessageDescription FIELD_WITH_MORE_THAN_ONE_INITIALIZER

FIELD_INIT_NOT_IN_JAVA_FILE

public static final MessageDescription FIELD_INIT_NOT_IN_JAVA_FILE

MODEL_FIELD_WITH_INITIALIZER

public static final MessageDescription MODEL_FIELD_WITH_INITIALIZER

EXTRANEOUS_ALSO

public static final MessageDescription EXTRANEOUS_ALSO

MISSING_ALSO

public static final MessageDescription MISSING_ALSO

MISSING_REFINING_ALSO

public static final MessageDescription MISSING_REFINING_ALSO

RECEIVER_IN_ASSIGNABLE

public static final MessageDescription RECEIVER_IN_ASSIGNABLE

NOT_ASSIGNABLE_FIELD

public static final MessageDescription NOT_ASSIGNABLE_FIELD

INVALID_MAPS_CLAUSE

public static final MessageDescription INVALID_MAPS_CLAUSE

INVALID_MODEL_FIELD_IN_ASSIGNABLE

public static final MessageDescription INVALID_MODEL_FIELD_IN_ASSIGNABLE

AMBIGUOUS_CALLABLE_METHOD

public static final MessageDescription AMBIGUOUS_CALLABLE_METHOD

NOT_CALLABLE_METHOD

public static final MessageDescription NOT_CALLABLE_METHOD

PURE_AND_ASSIGNABLE

public static final MessageDescription PURE_AND_ASSIGNABLE

PURE_AND_CALLS_NON_PURE

public static final MessageDescription PURE_AND_CALLS_NON_PURE

SYNCHRONIZED_PURE

public static final MessageDescription SYNCHRONIZED_PURE

JAVADOC_FAILURE

public static final MessageDescription JAVADOC_FAILURE

NULLABLE_NON_NULL_TOGETHER

public static final MessageDescription NULLABLE_NON_NULL_TOGETHER

CLASS_LEVEL_NULLABLE_NON_NULL_TOGETHER

public static final MessageDescription CLASS_LEVEL_NULLABLE_NON_NULL_TOGETHER

MODEL_FIELD_ACCESS

public static final MessageDescription MODEL_FIELD_ACCESS

GHOST_FIELD_ACCESS

public static final MessageDescription GHOST_FIELD_ACCESS

CLASS_NOT_DEFINED

public static final MessageDescription CLASS_NOT_DEFINED

METHOD_NOT_DEFINED

public static final MessageDescription METHOD_NOT_DEFINED

MISSING_REPRESENTS

public static final MessageDescription MISSING_REPRESENTS

METHOD_SPEC_INCONSISTENT

public static final MessageDescription METHOD_SPEC_INCONSISTENT

INVARIANT_FALSE

public static final MessageDescription INVARIANT_FALSE

ASSERTIONS_FOR_MORE_THAN_ONE_VAR

public static final MessageDescription ASSERTIONS_FOR_MORE_THAN_ONE_VAR

BAD_PARAM_MOD_ORDER

public static final MessageDescription BAD_PARAM_MOD_ORDER

BAD_SPEC_BODY_ORDER

public static final MessageDescription BAD_SPEC_BODY_ORDER

UNSAFE_ARITHMETIC_OPERATION

public static final MessageDescription UNSAFE_ARITHMETIC_OPERATION

SPEC_DISCARDED_SEMI

public static final MessageDescription SPEC_DISCARDED_SEMI

SPEC_DISCARDED_BLOCKEND

public static final MessageDescription SPEC_DISCARDED_BLOCKEND

SUBCLASSING_CONTRACT

public static final MessageDescription SUBCLASSING_CONTRACT

METHOD_NOT_PURE

public static final MessageDescription METHOD_NOT_PURE

NO_ASSIGNABLE

public static final MessageDescription NO_ASSIGNABLE

NON_MATCHING_PARAMETER_NAME

public static final MessageDescription NON_MATCHING_PARAMETER_NAME

METHOD_MAY_NOT_PURE

public static final MessageDescription METHOD_MAY_NOT_PURE

PARAMETER_NULLITY_MISMATCH

public static final MessageDescription PARAMETER_NULLITY_MISMATCH

UNEXPECTED_NULLITY_ANNOTATION

public static final MessageDescription UNEXPECTED_NULLITY_ANNOTATION

METHOD_NON_NULL_IN_SUPER

public static final MessageDescription METHOD_NON_NULL_IN_SUPER

IMPLICIT_NULLITY

public static final MessageDescription IMPLICIT_NULLITY

ARRAY_NULLITY_DECLARATION_MISMATCH

public static final MessageDescription ARRAY_NULLITY_DECLARATION_MISMATCH

PARSING

public static final MessageDescription PARSING

TYPECHECKING

public static final MessageDescription TYPECHECKING

ASSIGNABLE_CHECKING

public static final MessageDescription ASSIGNABLE_CHECKING

NOT_ADMISSIBLE

public static final MessageDescription NOT_ADMISSIBLE

NOT_ADMISSIBLE_REP_FIELD_PRIVATE

public static final MessageDescription NOT_ADMISSIBLE_REP_FIELD_PRIVATE

NOT_ADMISSIBLE_REP_METHOD_PRIVATE

public static final MessageDescription NOT_ADMISSIBLE_REP_METHOD_PRIVATE

ADMISSIBILITY_OBJECT_CREATION_NOT_SUPPORTED

public static final MessageDescription ADMISSIBILITY_OBJECT_CREATION_NOT_SUPPORTED

ADMISSIBILITY_METHOD_CALL_NOT_SUPPORTED

public static final MessageDescription ADMISSIBILITY_METHOD_CALL_NOT_SUPPORTED

ADMISSIBILITY_STATICS_NOT_SUPPORTED

public static final MessageDescription ADMISSIBILITY_STATICS_NOT_SUPPORTED

JmlMessages

public JmlMessages()