org.jmlspecs.jml4.ast
Class JmlSpecCaseBlock

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

All Implemented Interfaces:

TypeConstants, TypeIds

public class JmlSpecCaseBlock
extends JmlSpecCaseRest

Field Summary

JmlSpecCaseBody[]

bodies

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

JmlSpecCaseBlock(JmlSpecCaseBody[] bodies)

Method Summary

void	analysePostcondition(MethodScope scope, FlowContext methodContext, FlowInfo flowInfo)
void	generateCheckOfPostcondition(BlockScope currentScope, AbstractMethodDeclaration methodDeclaration, CodeStream codeStream)
java.util.List	getEnsuresExpressions()
java.lang.StringBuffer	print(int indent, java.lang.StringBuffer output)
void	resolve(MethodScope 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

bodies

public final JmlSpecCaseBody[] bodies

Constructor Detail

JmlSpecCaseBlock

public JmlSpecCaseBlock(JmlSpecCaseBody[] bodies)

Method Detail

analysePostcondition

public void analysePostcondition(MethodScope scope,
                                 FlowContext methodContext,
                                 FlowInfo flowInfo)

Specified by:

analysePostcondition in class JmlSpecCaseRest

generateCheckOfPostcondition

public void generateCheckOfPostcondition(BlockScope currentScope,
                                         AbstractMethodDeclaration methodDeclaration,
                                         CodeStream codeStream)

Specified by:

generateCheckOfPostcondition in class JmlSpecCaseRest

resolve

public void resolve(MethodScope scope)

Specified by:

resolve in class JmlSpecCaseRest

print

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

Specified by:

print in class ASTNode

getEnsuresExpressions

public java.util.List getEnsuresExpressions()

Specified by:

getEnsuresExpressions in class JmlSpecCaseRest

traverse

public void traverse(ASTVisitor visitor,
                     BlockScope scope)

Overrides:

traverse in class ASTNode