org.jmlspecs.jml4.ast
Class JmlLoopAnnotations

java.lang.Object
  org.eclipse.jdt.internal.compiler.ast.ASTNode
      org.jmlspecs.jml4.ast.JmlLoopAnnotations

All Implemented Interfaces:

TypeConstants, TypeIds

public class JmlLoopAnnotations
extends ASTNode

Field Summary

static JmlLoopInvariant[]	EMPTY_INVARIANTS
static JmlLoopVariant[]	EMPTY_VARIANTS
JmlLoopInvariant[]	invariants
JmlLoopVariant[]	variants

Fields inherited from class org.eclipse.jdt.internal.compiler.ast.ASTNode

Bit1, Bit10, Bit11, Bit12, Bit13, Bit14, Bit15, Bit16, Bit17, Bit18, Bit19, Bit2, Bit20, Bit21, Bit22, Bit23, Bit24, Bit25, Bit26, Bit27, Bit28, Bit29, Bit3, Bit30, Bit31, Bit32, Bit32L, Bit33L, Bit34L, Bit35L, Bit36L, Bit37L, Bit38L, Bit39L, Bit4, Bit40L, Bit41L, Bit42L, Bit43L, Bit44L, Bit45L, Bit46L, Bit47L, Bit48L, Bit49L, Bit5, Bit50L, Bit51L, Bit52L, Bit53L, Bit54L, Bit55L, Bit56L, Bit57L, Bit58L, Bit59L, Bit6, Bit60L, Bit61L, Bit62L, Bit63L, Bit64L, Bit7, Bit8, Bit9, bits, BlockExit, ContainsAssertion, DepthMASK, DepthSHIFT, DidResolve, DisableUnnecessaryCastCheck, DiscardEnclosingInstance, DocumentedFallthrough, Empty, ErrorInSignature, FirstAssignmentToLocal, GenerateCheckcast, HasAbstractMethods, HasAllMethodBodies, HasBeenGenerated, HasBeenResolved, HasLocalType, IgnoreNoEffectAssignCheck, IgnoreRawTypeCheck, InsideJavadoc, INVOCATION_ARGUMENT_OK, INVOCATION_ARGUMENT_UNCHECKED, INVOCATION_ARGUMENT_WILDCARD, IsAnnotationDefaultValue, IsAnonymousType, IsAnySubRoutineEscaping, IsCompoundAssigned, IsDefaultConstructor, IsElseIfStatement, IsImplicitThis, IsImplicitUnit, IsLocalDeclarationReachable, IsLocalType, IsMemberType, IsNonNull, IsReachable, IsRecovered, IsReturnedValue, IsSecondaryType, IsStrictlyAssigned, IsSubRoutineEscaping, IsSuperType, IsSynchronized, IsTryBlockExiting, IsUsefulEmptyStatement, IsVarArgs, LabelUsed, NeededScope, NeedFreeReturn, OnDemand, OperatorMASK, OperatorSHIFT, OverridingMethodWithSupercall, ParenthesizedMASK, ParenthesizedSHIFT, RestrictiveFlagMASK, ReturnTypeIDMASK, sourceEnd, sourceStart, SuperAccess, ThenExit, UndocumentedEmptyBlock, UnnecessaryCast, UnsafeCast, Used

Fields inherited from interface org.eclipse.jdt.internal.compiler.lookup.TypeConstants

ANNOTATION, ANNOTATION_PREFIX, ANNOTATION_SUFFIX, ANONYM_PREFIX, ANONYM_SUFFIX, BOOLEAN, BYTE, CHAR, CharArray_JAVA_IO_OBJECTINPUTSTREAM, CharArray_JAVA_IO_OBJECTOUTPUTSTREAM, CharArray_JAVA_IO_OBJECTSTREAMFIELD, CharArray_JAVA_LANG_ANNOTATION_ANNOTATION, CharArray_JAVA_LANG_ENUM, CharArray_JAVA_LANG_OBJECT, CLINIT, CLONE, CONSTRAINT_EQUAL, CONSTRAINT_EXTENDS, CONSTRAINT_SUPER, DOUBLE, FLOAT, GETCLASS, INIT, INT, IO, JAVA, JAVA_IO, JAVA_IO_EXTERNALIZABLE, JAVA_IO_IOEXCEPTION, JAVA_IO_OBJECTINPUTSTREAM, JAVA_IO_OBJECTOUTPUTSTREAM, JAVA_IO_OBJECTSTREAMEXCEPTION, JAVA_IO_PRINTSTREAM, JAVA_IO_SERIALIZABLE, JAVA_LANG, JAVA_LANG_ANNOTATION_ANNOTATION, JAVA_LANG_ANNOTATION_DOCUMENTED, JAVA_LANG_ANNOTATION_ELEMENTTYPE, JAVA_LANG_ANNOTATION_INHERITED, JAVA_LANG_ANNOTATION_RETENTION, JAVA_LANG_ANNOTATION_RETENTIONPOLICY, JAVA_LANG_ANNOTATION_TARGET, JAVA_LANG_ASSERTIONERROR, JAVA_LANG_BOOLEAN, JAVA_LANG_BYTE, JAVA_LANG_CHARACTER, JAVA_LANG_CLASS, JAVA_LANG_CLASSNOTFOUNDEXCEPTION, JAVA_LANG_CLONEABLE, JAVA_LANG_DEPRECATED, JAVA_LANG_DOUBLE, JAVA_LANG_ENUM, JAVA_LANG_ERROR, JAVA_LANG_EXCEPTION, JAVA_LANG_FLOAT, JAVA_LANG_ILLEGALARGUMENTEXCEPTION, JAVA_LANG_INTEGER, JAVA_LANG_ITERABLE, JAVA_LANG_LONG, JAVA_LANG_NOCLASSDEFERROR, JAVA_LANG_OBJECT, JAVA_LANG_OVERRIDE, JAVA_LANG_REFLECT_CONSTRUCTOR, JAVA_LANG_REFLECT_FIELD, JAVA_LANG_REFLECT_METHOD, JAVA_LANG_RUNTIMEEXCEPTION, JAVA_LANG_SHORT, JAVA_LANG_STRING, JAVA_LANG_STRINGBUFFER, JAVA_LANG_STRINGBUILDER, JAVA_LANG_SUPPRESSWARNINGS, JAVA_LANG_SYSTEM, JAVA_LANG_THROWABLE, JAVA_LANG_VOID, JAVA_UTIL_ITERATOR, JML_ANNOTATION, JML_ANNOTATION_CODE_BIGINT_MATH, JML_ANNOTATION_CODE_JAVA_MATH, JML_ANNOTATION_CODE_SAFE_MATH, JML_ANNOTATION_GHOST, JML_ANNOTATION_HELPER, JML_ANNOTATION_INSTANCE, JML_ANNOTATION_MODEL, JML_ANNOTATION_NON_NULL, JML_ANNOTATION_NON_NULL_BY_DEFAULT, JML_ANNOTATION_NULLABLE, JML_ANNOTATION_NULLABLE_BY_DEFAULT, JML_ANNOTATION_PEER, JML_ANNOTATION_PKG, JML_ANNOTATION_PURE, JML_ANNOTATION_READONLY, JML_ANNOTATION_REP, JML_ANNOTATION_SPEC_BIGINT_MATH, JML_ANNOTATION_SPEC_JAVA_MATH, JML_ANNOTATION_SPEC_PROTECTED, JML_ANNOTATION_SPEC_PUBLIC, JML_ANNOTATION_SPEC_SAFE_MATH, JML_ANNOTATION_TYPE_CODE_BIGINT_MATH, JML_ANNOTATION_TYPE_CODE_JAVA_MATH, JML_ANNOTATION_TYPE_CODE_SAFE_MATH, JML_ANNOTATION_TYPE_GHOST, JML_ANNOTATION_TYPE_HELPER, JML_ANNOTATION_TYPE_INSTANCE, JML_ANNOTATION_TYPE_MODEL, JML_ANNOTATION_TYPE_NON_NULL_BY_DEFAULT, JML_ANNOTATION_TYPE_NONNULL, JML_ANNOTATION_TYPE_NULLABLE, JML_ANNOTATION_TYPE_NULLABLE_BY_DEFAULT, JML_ANNOTATION_TYPE_PEER, JML_ANNOTATION_TYPE_PURE, JML_ANNOTATION_TYPE_READONLY, JML_ANNOTATION_TYPE_REP, JML_ANNOTATION_TYPE_SPEC_BIGINT_MATH, JML_ANNOTATION_TYPE_SPEC_JAVA_MATH, JML_ANNOTATION_TYPE_SPEC_PROTECTED, JML_ANNOTATION_TYPE_SPEC_PUBLIC, JML_ANNOTATION_TYPE_SPEC_SAFE_MATH, JML_ANNOTATION_TYPE_UNINITIALIZED, JML_ANNOTATION_UNINITIALIZED, JML_ORG, JML_RUNTIME, JML_RUNTIME_ANNOTATION, JML4, JMLSPECS, LANG, LENGTH, LONG, MAIN, MISMATCH, NULL, OBJECT, OK, PACKAGE_INFO_NAME, READOBJECT, READRESOLVE, REFLECT, SERIALPERSISTENTFIELDS, SERIALVERSIONUID, SHORT, SYNTHETIC_ACCESS_METHOD_PREFIX, SYNTHETIC_ASSERT_DISABLED, SYNTHETIC_CLASS, SYNTHETIC_ENCLOSING_INSTANCE_PREFIX, SYNTHETIC_ENUM_VALUES, SYNTHETIC_OUTER_LOCAL_PREFIX, SYNTHETIC_SWITCH_ENUM_TABLE, TYPE, UNCHECKED, UPPER_ANNOTATION_TYPE, UPPER_CLASS, UPPER_CONSTRUCTOR, UPPER_FIELD, UPPER_LOCAL_VARIABLE, UPPER_METHOD, UPPER_PACKAGE, UPPER_PARAMETER, UPPER_RUNTIME, UPPER_SOURCE, UTIL, VALUE, VALUEOF, VALUES, VOID, WILDCARD_CAPTURE, WILDCARD_CAPTURE_NAME_PREFIX, WILDCARD_CAPTURE_NAME_SUFFIX, WILDCARD_EXTENDS, WILDCARD_MINUS, WILDCARD_NAME, WILDCARD_PLUS, WILDCARD_STAR, WILDCARD_SUPER, WRITEOBJECT, WRITEREPLACE

Fields inherited from interface org.eclipse.jdt.internal.compiler.lookup.TypeIds

Boolean2Boolean, Boolean2Int, Boolean2String, BOXING, Byte2Byte, Byte2Char, Byte2Double, Byte2Float, Byte2Int, Byte2Long, Byte2Short, Byte2String, Char2Byte, Char2Char, Char2Double, Char2Float, Char2Int, Char2Long, Char2Short, Char2String, COMPILE_TYPE_MASK, Double2Byte, Double2Char, Double2Double, Double2Float, Double2Int, Double2Long, Double2Short, Double2String, Float2Byte, Float2Char, Float2Double, Float2Float, Float2Int, Float2Long, Float2Short, Float2String, IMPLICIT_CONVERSION_MASK, Int2Byte, Int2Char, Int2Double, Int2Float, Int2Int, Int2Long, Int2Short, Int2String, Long2Byte, Long2Char, Long2Double, Long2Float, Long2Int, Long2Long, Long2Short, Long2String, NoId, Null2String, Object2Object, Object2String, Short2Byte, Short2Char, Short2Double, Short2Float, Short2Int, Short2Long, Short2Short, Short2String, String2String, T_boolean, T_byte, T_char, T_double, T_float, T_int, T_JavaIoException, T_JavaIoExternalizable, T_JavaIoObjectStreamException, T_JavaIoPrintStream, T_JavaIoSerializable, T_JavaLangAnnotationAnnotation, T_JavaLangAnnotationDocumented, T_JavaLangAnnotationElementType, T_JavaLangAnnotationInherited, T_JavaLangAnnotationRetention, T_JavaLangAnnotationRetentionPolicy, T_JavaLangAnnotationTarget, T_JavaLangAssertionError, T_JavaLangBoolean, T_JavaLangByte, T_JavaLangCharacter, T_JavaLangClass, T_JavaLangClassNotFoundException, T_JavaLangCloneable, T_JavaLangDeprecated, T_JavaLangDouble, T_JavaLangEnum, T_JavaLangError, T_JavaLangException, T_JavaLangFloat, T_JavaLangIllegalArgumentException, T_JavaLangInteger, T_JavaLangIterable, T_JavaLangLong, T_JavaLangNoClassDefError, T_JavaLangObject, T_JavaLangOverride, T_JavaLangReflectConstructor, T_JavaLangReflectField, T_JavaLangReflectMethod, T_JavaLangRuntimeException, T_JavaLangShort, T_JavaLangString, T_JavaLangStringBuffer, T_JavaLangStringBuilder, T_JavaLangSuppressWarnings, T_JavaLangSystem, T_JavaLangThrowable, T_JavaLangVoid, T_JavaUtilIterator, T_long, T_null, T_short, T_undefined, T_void, UNBOXING

Constructor Summary

JmlLoopAnnotations(JmlLoopInvariant[] invariants)

JmlLoopAnnotations(JmlLoopInvariant[] invariants, JmlLoopVariant[] variants)

JmlLoopAnnotations(JmlLoopVariant[] variants)

Method Summary

void	analyseCode(BlockScope currentScope, FlowContext flowContext, FlowInfo flowInfo)
void	checkLoopInvariant(BlockScope currentScope, CodeStream codeStream)
void	checkLoopVariant(BlockScope currentScope, CodeStream codeStream, LocalVariableBinding firstTimeBinding)
void	initVariantStore(BlockScope currentScope, CodeStream codeStream)
java.lang.StringBuffer	print(int indent, java.lang.StringBuffer output)
void	resolve(BlockScope scope)
void	traverse(ASTVisitor visitor, BlockScope scope)

Methods inherited from class org.eclipse.jdt.internal.compiler.ast.ASTNode

checkInvocationArguments, concreteStatement, isFieldUseDeprecated, isImplicitThis, isMethodUseDeprecated, isSuper, isThis, isTypeUseDeprecated, printAnnotations, printIndent, printModifiers, resolveAnnotations, resolveDeprecatedAnnotations, sourceEnd, sourceStart, toString

Methods inherited from class java.lang.Object

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

Field Detail

EMPTY_INVARIANTS

public static final JmlLoopInvariant[] EMPTY_INVARIANTS

EMPTY_VARIANTS

public static final JmlLoopVariant[] EMPTY_VARIANTS

invariants

public final JmlLoopInvariant[] invariants

variants

public final JmlLoopVariant[] variants

Constructor Detail

JmlLoopAnnotations

public JmlLoopAnnotations(JmlLoopInvariant[] invariants)

JmlLoopAnnotations

public JmlLoopAnnotations(JmlLoopVariant[] variants)

JmlLoopAnnotations

public JmlLoopAnnotations(JmlLoopInvariant[] invariants,
                          JmlLoopVariant[] variants)

Method Detail

print

public java.lang.StringBuffer print(int indent,
                                    java.lang.StringBuffer output)

Specified by:

print in class ASTNode

checkLoopInvariant

public void checkLoopInvariant(BlockScope currentScope,
                               CodeStream codeStream)

checkLoopVariant

public void checkLoopVariant(BlockScope currentScope,
                             CodeStream codeStream,
                             LocalVariableBinding firstTimeBinding)

resolve

public void resolve(BlockScope scope)

analyseCode

public void analyseCode(BlockScope currentScope,
                        FlowContext flowContext,
                        FlowInfo flowInfo)

initVariantStore

public void initVariantStore(BlockScope currentScope,
                             CodeStream codeStream)

traverse

public void traverse(ASTVisitor visitor,
                     BlockScope scope)

Overrides:

traverse in class ASTNode