jml2b.structure.java
Class Type

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.java.ParsedItem
          jml2b.structure.java.Type

All Implemented Interfaces:

IType, jml.JmlDeclParserTokenTypes, Linkable, java.io.Serializable

Direct Known Subclasses:

JavaType

public class Type

extends ParsedItem

implements Linkable, jml.JmlDeclParserTokenTypes, java.io.Serializable, IType

Class representing types. Types can correspond to builtin types (int, short, etc...), reference types (correspoding to references to classes) or array types. Types contains a tag that describes the type information available. The tag can be equal to:

• T_VOID, only used for describing return values. Correspond to the void return value.
• T_BOOLEAN, indicating that the type corresponds to the boolean builtin type.
• T_BYTE, indicating that the type corresponds to the byte builtin type.
• T_SHORT, indicating that the type corresponds to the short builtin type.
• T_CHAR, indicating that the type corresponds to the char builtin type.
• T_DOUBLE, indicating that the type corresponds to the double builtin type.
• T_FLOAT, indicating that the type corresponds to the float builtin type.
• T_INT, indicating that the type corresponds to the int builtin type.
• T_LONG, indicating that the type corresponds to the long builtin type.
• T_NULL, indicating that the type corresponds to a null reference. Such type should never occur in a signature, and is only used internally.
• T_TYPE, indicating that the type corresponds to a type. The jml \type operator can produce such types.
• T_REF, indicating that the type corresponds to a reference to a class. The corresponding class can be accessed using the getRefType method.
• T_ARRAY, indicating that the type corresponds to a reference to an array. The type describing the elements stored within the array is obtained using the getElemType method. For those types, the getRefType method can be called and will return the special "array" class.

Author:

A. Requet L. Burdy

See Also:

Type#getRefType();, Type#getElemType();, Serialized Form

Field Summary

static int	T_ARRAY indicate an array type.
static int	T_BOOLEAN Constant representing the boolean type.
static int	T_BYTE Constant representing the byte type.
static int	T_CHAR Constant representing the char type.
static int	T_CLASS used for typing class expression: this should always result in a typecheck error
static int	T_DOUBLE Constant representing the double type.
static int	T_FLOAT Constant representing the float type.
static int	T_INT Constant representing the int type.
static int	T_LONG Constant representing the long type.
static int	T_NULL Constant representing the null type.
static int	T_REF Constant used to tag references to classes.
static int	T_SHORT Constant representing the short type.
static int	T_TYPE used for return values of \elemtype and \type
static int	T_VOID Constant representing the void type.

Fields inherited from interface jml2b.link.Linkable

STATE_LINKED, STATE_LINKED_STATEMENTS, STATE_LINKED_TYPE_CHECKED, STATE_UNLINKED

Fields inherited from interface jml.JmlDeclParserTokenTypes

ABRUPT_BEHAVIOR, ACCESSIBLE, ACCESSIBLE_KEYWORD, ACCESSIBLE_REDUNDANTLY, ACCESSIBLE_SEQ, ADDITIVE_ASSIGNMENT_OP, ADDITIVE_OP, AFFIRM_KEYWORD, ALSO, AND, ARRAY_DECLARATOR, ASGNABLE_SEQ, ASSERT, ASSERT_REDUNDANTLY, ASSIGN, ASSIGNABLE, ASSIGNABLE_KEYWORD, ASSIGNABLE_REDUNDANTLY, ASSUME, ASSUME_KEYWORD, ASSUME_REDUNDANTLY, AXIOM, BACKWARD_IMPLIES, BADCHAR, BAND, BAND_ASSIGN, BEHAVIOR, BITWISE_ASSIGNMENT_OP, BITWISE_OP, BNOT, BOR, BOR_ASSIGN, BREAKS, BREAKS_KEYWORD, BREAKS_REDUNDANTLY, BREAKS_SEQ, BSR, BSR_ASSIGN, BXOR, BXOR_ASSIGN, CALLABLE, CALLABLE_KEYWORD, CALLABLE_REDUNDANTLY, CALLABLE_SEQ, CASE, CAST, CHAR_LITERAL, CHOOSE, CHOOSE_IF, COLON, COMMA, CONJOINABLE_SPEC, CONSTRAINT, CONSTRAINT_KEYWORD, CONSTRAINT_REDUNDANTLY, CONSTRUCTOR, CONT_SEQ, CONTINUES, CONTINUES_KEYWORD, CONTINUES_REDUNDANTLY, DEC, DECREASES, DECREASES_REDUNDANTLY, DECREASING, DECREASING_KEYWORD, DECREASING_REDUNDANTLY, DEPENDS, DEPENDS_KEYWORD, DEPENDS_REDUNDANTLY, DIM_EXPRS, DIMS, DINFORMALLY, DIV, DIV_ASSIGN, DIV_SEQ, DIVERGES, DIVERGES_KEYWORD, DIVERGES_REDUNDANTLY, DOC_ATSIGN, DOC_ATSIGN_KEYWORD, DOC_AUTHOR, DOC_COMMENT, DOC_COMMENT_START, DOC_DEPRECATED, DOC_EXCEPTION, DOC_JML_SPECS, DOC_NL_WS, DOC_NON_EMPTY_TEXTLINE, DOC_NON_NL_WS, DOC_PARAM, DOC_RETURN, DOC_SEE, DOC_SERIAL, DOC_SERIALDATA, DOC_SERIALFIELD, DOC_SINCE, DOC_THROWS, DOC_UNKNOWN_KEYWORD, DOC_VERSION, DOT, DOT_DOT, ELSE, ENS_SEQ, ENSURES, ENSURES_KEYWORD, ENSURES_REDUNDANTLY, EOF, EQUAL, EQUALITY_OP, EQUIV, EQUIVALENCE_OP, ESC, EXAMPLE, EXCEPTIONAL_BEHAVIOR, EXCEPTIONAL_EXAMPLE, EXPONENT, EXSURES, EXSURES_REDUNDANTLY, EXT_ALSO, EXT_AND, FLOAT_SUFFIX, FOR, FOR_EXAMPLE, FOR_INIT, FOR_TEST, FOR_UPDATER, FORALL, GE, GHOST, GT, HENCE_BY, HENCE_BY_KEYWORD, HENCE_BY_REDUNDANTLY, HEX_DIGIT, IDENT, IGNORED_AT_IN_COMMENT, IMPLICATION_OP, IMPLIES_THAT, INC, INFORMAL_DESCRIPTION, INIT, INITIALIZER, INITIALLY, INSTANCE, INSTANCE_INIT, INVARIANT, INVARIANT_KEYWORD, INVARIANT_REDUNDANTLY, IS_SUBTYPE_OF, JAVA_BUILTIN_TYPE, JAVA_MODIFIER, JML_BACKSLASH_SEQUENCE, JML_MODIFIER, L_ARROW, LABEL, LABEL_KEYWORD, LAND, LBRACK, LCURLY, LCURLY_VBAR, LE, LET, LETOLD_KEYWORD, LIMPLIES, LITERAL_abstract, LITERAL_assert, LITERAL_boolean, LITERAL_break, LITERAL_byte, LITERAL_case, LITERAL_catch, LITERAL_char, LITERAL_class, LITERAL_const, LITERAL_continue, LITERAL_default, LITERAL_do, LITERAL_double, LITERAL_else, LITERAL_extends, LITERAL_false, LITERAL_final, LITERAL_finally, LITERAL_float, LITERAL_for, LITERAL_if, LITERAL_implements, LITERAL_import, LITERAL_instanceof, LITERAL_int, LITERAL_interface, LITERAL_long, LITERAL_native, LITERAL_new, LITERAL_null, LITERAL_package, LITERAL_private, LITERAL_protected, LITERAL_public, LITERAL_return, LITERAL_short, LITERAL_static, LITERAL_strictfp, LITERAL_super, LITERAL_switch, LITERAL_synchronized, LITERAL_this, LITERAL_throw, LITERAL_throws, LITERAL_transient, LITERAL_true, LITERAL_try, LITERAL_void, LITERAL_volatile, LITERAL_while, LNOT, LOGICAL_OP, LOOP_ASGNABLE_SEQ, LOOP_ASSIGNABLE_KEYWORD, LOOP_EXSURES, LOOP_INV_SEQ, LOOP_INVARIANT, LOOP_INVARIANT_REDUNDANTLY, LOOP_MODIFIES, LOOP_SIG_SEQ, LOR, LPAREN, LT, MAINTAINING, MAINTAINING_KEYWORD, MAINTAINING_REDUNDANTLY, MEASURED_BY, MEASURED_BY_KEYWORD, MEASURED_BY_REDUNDANTLY, METH, MINUS, MINUS_ASSIGN, ML_COMMENT, MOD, MOD_ASSIGN, MODEL, MODEL_PROGRAM, MODIFIABLE, MODIFIABLE_REDUNDANTLY, MODIFIER_SET, MODIFIES, MODIFIES_REDUNDANTLY, MONITORED, MONITORED_BY, MULTIPLICATIVE_ASSIGNMENT_OP, MULTIPLICATIVE_OP, NESTED_CLASS, NL_WS, NON_NL_WS, NON_NULL, NORMAL_BEHAVIOR, NORMAL_EXAMPLE, NOT_EQUAL, NOT_EQUIV, NOWARN_LABEL, NOWARN_LABEL_LIST, NULL_TREE_LOOKAHEAD, NUM_FLOAT, NUM_INT, OLD, OR, PARAM, PLUS, PLUS_ASSIGN, POST, POST_DEC, POST_INC, POST_INCREMENT_OP, POST_REDUNDANTLY, PRE, PRE_INCREMENT_OP, PRE_REDUNDANTLY, PRIVACY_MODIFIER, PURE, QUANT_VARS, QUANTIFIED_EXPR, QUANTIFIER_TOKEN, QUESTION, R_ARROW, RBRACK, RCURLY, READABLE_IF, REFINE, RELATIONAL_OP, REPLACE, REPRESENTS, REPRESENTS_KEYWORD, REPRESENTS_REDUNDANTLY, REQUIRES, REQUIRES_KEYWORD, REQUIRES_REDUNDANTLY, RETURNS, RETURNS_KEYWORD, RETURNS_REDUNDANTLY, RETURNS_SEQ, RPAREN, SEMI, SET, SET_COMPR, SHIFT_ASSIGNMENT_OP, SHIFT_OP, SIG_SEQ, SIGNALS, SIGNALS_KEYWORD, SIGNALS_REDUNDANTLY, SL, SL_ASSIGN, SL_COMMENT, SPEC_CASE, SPEC_PROTECTED, SPEC_PUBLIC, SPEC_SL_COMMENT, SPEC_STATEMENT, SR, SR_ASSIGN, STAR, STAR_ASSIGN, STAR_ELEMS, STATIC_INITIALIZER, STRING_LITERAL, SUBCLASSING_CONTRACT, T_ELEMTYPE, T_EVERYTHING, T_EXISTS, T_FIELDS_OF, T_FORALL, T_FRESH, T_INVARIANT_FOR, T_IS_INITIALIZED, T_LBLNEG, T_LBLPOS, T_LOCKSET, T_MAX, T_MIN, T_NONNULLELEMENTS, T_NOT_MODIFIED, T_NOT_SPECIFIED, T_NOTHING, T_NUM_OF, T_OLD, T_OTHER, T_PRODUCT, T_REACH, T_RESULT, T_SUCH_THAT, T_SUM, T_TYPEOF, T_TYPEOFALLTYPES, UNARY_NUMERIC_OP, UNINITIALIZED, UNREACHABLE, VAR_DECL, VBAR_RCURLY, VF_SEQ, VOCAB, WEAKLY, WHEN, WHEN_KEYWORD, WHEN_REDUNDANTLY, WS

Constructor Summary

Type()

Type(AClass cl)
Creates a new type corresponding to the given class.

Type(IJml2bConfiguration config, Type t)
Creates a new array class containing the given elements.

Type(int tag)
Creates a new builtin type with the given tag.

Type(JmlFile jf, antlr.collections.AST tree)
Creates a new type from the given AST.

Type(java.lang.String typeDescriptor)

Type(Type t)
Creates a new array type using the given type as elements.

Method Summary

static Type	addDims(JmlFile jmlFile, antlr.collections.AST dims_ast, Type t) count the number of dimensions in the given ast.
static Type	binaryNumericPromotion(Type t1, Type t2)
static void	clearAll() Sets typeObject to null.
static Type	createUnlinkedClass(java.lang.String fqn) Creates an unlinked type element corresponding to the given fully qualified class name.
boolean	equals(java.lang.Object o)
boolean	equals(Type t)
static Type	getBoolean() Returns a type corresponding to the boolean builtin type.
static Type	getByte()
static Type	getChar() Returns a type corresponding to the char builtin type.
int	getDimension() return the dimension of the type.
Type	getElemType() Returns the type of the elements of an array type.
static Type	getInteger() Returns a type corresponding to the int builtin type.
static Type	getObject(IJml2bConfiguration config) Returns a type corresponding to the java.lang.Object class.
AClass	getRefType() Returns the reference type for references or array types.
static Type	getShort()
int	getTag() Returns the tag describing the type of the type.
AClass	getTargetedClass() Returns the class that is the type of the object or of the element of the type if it is an array.
static Type	getType() Returns a type corresponding to the type builtin type.
boolean	isArray() Returns true if this type correspond to an array type.
boolean	isBoolean()
boolean	isBuiltin() Returns true if the type is a builtin-type.
boolean	isIntegral()
boolean	isNumeric()
boolean	isRef()
boolean	isSubtypeOf(Type t) return true iff this is a subtype of the given type.
void	link(IJml2bConfiguration config, LinkContext f)
int	linkStatements(IJml2bConfiguration config, LinkContext f)
antlr.collections.AST	parse(antlr.collections.AST type_ast) create a type from the given AST.
void	setBuiltin(int type_tag) Set the current type to represent a builtin type of the type type_tag.
boolean	setBuiltin(java.lang.String type_name) Set the current type to represent a builtin type of the typ described by the given string.
void	setParsedItem(ParsedItem pi)
static java.lang.String	signatureToString(java.util.Enumeration e) Converts a signature to a string suitable for printing.
java.lang.String	toJava() Converts the type to a java representation.
ITranslationResult	toLang(java.lang.String language)
java.lang.String	toString()
Type	unaryPromote()

Methods inherited from class jml2b.structure.java.ParsedItem

change, change, getColumn, getJmlFile, getLine, save, setBox

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

T_INT

public static final int T_INT

Constant representing the int type.

See Also:

Constant Field Values

T_SHORT

public static final int T_SHORT

Constant representing the short type.

See Also:

Constant Field Values

T_BYTE

public static final int T_BYTE

Constant representing the byte type.

See Also:

Constant Field Values

T_BOOLEAN

public static final int T_BOOLEAN

Constant representing the boolean type.

See Also:

Constant Field Values

T_CHAR

public static final int T_CHAR

Constant representing the char type.

See Also:

Constant Field Values

T_REF

public static final int T_REF

Constant used to tag references to classes. For types that have this tag, information on the referenced class can be obtained using the getRefType() method.

See Also:

Type#getRefType();, Constant Field Values

T_ARRAY

public static final int T_ARRAY

indicate an array type. For types that have this tag, information on the element type can be obtained using the getElemType() method. Additionally, the getRefType() method can be called and will return the special "array" class.

See Also:

Type#getElemType();, Type#getRefType();, Constant Field Values

T_VOID

public static final int T_VOID

Constant representing the void type.

See Also:

Constant Field Values

T_FLOAT

public static final int T_FLOAT

Constant representing the float type.

See Also:

Constant Field Values

T_LONG

public static final int T_LONG

Constant representing the long type.

See Also:

Constant Field Values

T_DOUBLE

public static final int T_DOUBLE

Constant representing the double type.

See Also:

Constant Field Values

T_NULL

public static final int T_NULL

Constant representing the null type. Although this type will not appear directly in the source code (i.e. it is not possible to declare variables having this type), it is required internally for the method lookup and type checking.

See Also:

Constant Field Values

T_TYPE

public static final int T_TYPE

used for return values of \elemtype and \type

See Also:

Constant Field Values

T_CLASS

public static final int T_CLASS

used for typing class expression: this should always result in a typecheck error

See Also:

Constant Field Values

Constructor Detail

Type

public Type()

Type

public Type(java.lang.String typeDescriptor)

Type

public Type(int tag)

Creates a new builtin type with the given tag. The tag should correspond to a builtin type and should not be equal to T_REF or T_ARRAY, since those tags requires additional information (reference type and array type).

Parameters:

tag - the builtin type.

Type

public Type(AClass cl)

Creates a new type corresponding to the given class. The resulting type will have tag T_REF, and its reference type will be set to cl.

Parameters:

cl - the class described by the resultin type. Should not be null.

Type

public Type(IJml2bConfiguration config,
            Type t)
     throws Jml2bException

Creates a new array class containing the given elements.

Parameters:

config - the configuration to use for loading new classes. It is required, since calling this constructor may theorically trigger the loading of the java.lang.Object class.

t - the type of the elements stored within the array. This parameter should not be null.

Type

public Type(Type t)

Creates a new array type using the given type as elements. This constructor does not requires a configuration, since it aims to be called during parsing, and does not initialize the element type.

The element type will be initialised later, during the linking phase. This constructor is called from the addDims method.

Parameters:

t - The type of the elements. Should not be null.

See Also:

addDims(JmlFile, AST, Type);

Type

public Type(JmlFile jf,
            antlr.collections.AST tree)

Creates a new type from the given AST.

Parameters:

jf - the file where the type occured.

tree - the AST corresponding to the type.

Method Detail

binaryNumericPromotion

public static Type binaryNumericPromotion(Type t1,
                                          Type t2)

parse

public antlr.collections.AST parse(antlr.collections.AST type_ast)
                            throws Jml2bException

create a type from the given AST. The AST must point to a type declaration.

Throws:

Jml2bException

equals

public boolean equals(Type t)

link

public void link(IJml2bConfiguration config,
                 LinkContext f)
          throws Jml2bException

Specified by:

link in interface Linkable

Throws:

Jml2bException

linkStatements

public int linkStatements(IJml2bConfiguration config,
                          LinkContext f)
                   throws Jml2bException

Specified by:

linkStatements in interface Linkable

Throws:

Jml2bException

getRefType

public AClass getRefType()

Returns the reference type for references or array types.

Specified by:

getRefType in interface IType

Returns:

Class the class of the reference type.

getElemType

public Type getElemType()

Returns the type of the elements of an array type. The current type should be an array type. That is it should have the tag T_ARRAY.

Specified by:

getElemType in interface IType

Returns:

Type the type of the elements that are stored within the array.

setBuiltin

public void setBuiltin(int type_tag)

Set the current type to represent a builtin type of the type type_tag.

Parameters:

type_tag - the type to which the type should be set. It should correspond to a primitive type.

setBuiltin

public boolean setBuiltin(java.lang.String type_name)

Set the current type to represent a builtin type of the typ described by the given string.

Parameters:

type_name - the name of the type.

Returns:

true on success, false if the string was not understood.

equals

public boolean equals(java.lang.Object o)

isArray

public boolean isArray()

Returns true if this type correspond to an array type.

Returns:

true if the type is an array type, false otherwise.

isBuiltin

public boolean isBuiltin()

Returns true if the type is a builtin-type. Note that the type T_TYPE is considered a builtin-type.

Returns:

true if the type is a builtin one, false otherwise.

isIntegral

public boolean isIntegral()

isNumeric

public boolean isNumeric()

isRef

public boolean isRef()

unaryPromote

public Type unaryPromote()

isBoolean

public boolean isBoolean()

getDimension

public int getDimension()

return the dimension of the type. If the type is not an array, then its dimension is equal to 0. Otherwise, it is equal to the dimension of the array.

Returns:

the dimension of the type.

getTargetedClass

public AClass getTargetedClass()

Returns the class that is the type of the object or of the element of the type if it is an array.

getTag

public int getTag()

Returns the tag describing the type of the type.

Specified by:

getTag in interface IType

Returns:

int the tag corresponding to the type.

createUnlinkedClass

public static Type createUnlinkedClass(java.lang.String fqn)

Creates an unlinked type element corresponding to the given fully qualified class name.

Parameters:

fqn - the fully qualified name of the class.

Returns:

a type describing the given class, that should be linked.

toJava

public java.lang.String toJava()

Converts the type to a java representation.

Returns:

String a string corresponding to the type using a Java-like notation.

isSubtypeOf

public boolean isSubtypeOf(Type t)

return true iff this is a subtype of the given type. That is if this can be converted implicitely to t. This method will return true in the case where the types are equals.

Parameters:

t - the type that should be compared.

Returns:

true if the current type is a subtype of t, false otherwise.

getObject

public static Type getObject(IJml2bConfiguration config)
                      throws Jml2bException

Returns a type corresponding to the java.lang.Object class.

Parameters:

config - the configuration that should be used for loading classes.

Returns:

Type the type representing the java.lang.Object class.

Throws:

Jml2bException

clearAll

public static void clearAll()

Sets typeObject to null. This method is called by Package.clearAll();

addDims

public static Type addDims(JmlFile jmlFile,
                           antlr.collections.AST dims_ast,
                           Type t)
                    throws Jml2bException

count the number of dimensions in the given ast.

Throws:

Jml2bException

signatureToString

public static java.lang.String signatureToString(java.util.Enumeration e)

Converts a signature to a string suitable for printing. The given enumeration should enumerate Type elements.

Parameters:

e - the enumeration corresponding to the signature.

Returns:

String a String representation of the signature.

getBoolean

public static Type getBoolean()

Returns a type corresponding to the boolean builtin type. This method is prefered to using new Type(T_BOOLEAN), since it reuses the same instance for each type, thus reducing memory use.

Returns:

Type a type describing the boolean builtin type.

getInteger

public static Type getInteger()

Returns a type corresponding to the int builtin type. This method is prefered to using new Type(T_INT), since it reuses the same instance for each type, thus reducing memory use.

Returns:

Type a type describing the int builtin type.

getChar

public static Type getChar()

Returns a type corresponding to the char builtin type. This method is prefered to using new Type(T_CHAR), since it reuses the same instance for each type, thus reducing memory use.

Returns:

Type a type describing the char builtin type.

getByte

public static Type getByte()

getShort

public static Type getShort()

getType

public static Type getType()

Returns a type corresponding to the type builtin type. This method is prefered to using new Type(T_TYPE), since it reuses the same instance for each type, thus reducing memory use.

Returns:

Type a type describing the type builtin type.

toString

public java.lang.String toString()

toLang

public ITranslationResult toLang(java.lang.String language)
                          throws LanguageException

Throws:

LanguageException

setParsedItem

public void setParsedItem(ParsedItem pi)