Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.checker
Class JmlConstructorDeclaration

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.util.compiler.Phylum
          extended byorg.multijava.mjc.JPhylum
              extended byorg.jmlspecs.checker.JmlNode
                  extended byorg.jmlspecs.checker.JmlMemberDeclaration
                      extended byorg.jmlspecs.checker.JmlMethodDeclaration
                          extended byorg.jmlspecs.checker.JmlConstructorDeclaration
All Implemented Interfaces:
Annotatable, Cloneable, Comparable, Constants, Constants, Constants, JConstructorDeclarationType, JMemberDeclarationType, JMethodDeclarationType, PhylumType
public class JmlConstructorDeclaration
extends JmlMethodDeclaration
implements JConstructorDeclarationType

JmlConstructorDeclaration.java

Version:
$Revision: 1.10 $
Author:
Curtis Clifton

Nested Class Summary
 
Nested classes inherited from class org.jmlspecs.checker.JmlNode
JmlNode.DummyInitializerDeclaration
 
Field Summary
private  JConstructorDeclaration delegee
           
private  CVariableInfoTable instanceInfo
          Temporarily stores the final field definite assignment information while typechecking the constructor.
 
Fields inherited from class org.jmlspecs.checker.JmlMethodDeclaration
 
Fields inherited from class org.jmlspecs.checker.JmlMemberDeclaration
refinedDecl, refiningDecl
 
Fields inherited from class org.jmlspecs.checker.JmlNode
MJCVISIT_MESSAGE
 
Fields inherited from class org.multijava.util.compiler.Phylum
 
Fields inherited from class org.multijava.util.Utils
DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO
 
Fields inherited from interface org.jmlspecs.checker.Constants
ACC2_RAC_METHOD, ACC_CODE, ACC_CODE_BIGINT_MATH, ACC_CODE_JAVA_MATH, ACC_CODE_SAFE_MATH, ACC_GHOST, ACC_HELPER, ACC_INSTANCE, ACC_MODEL, ACC_MONITORED, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_QUERY, ACC_SECRET, ACC_SPEC_BIGINT_MATH, ACC_SPEC_JAVA_MATH, ACC_SPEC_PROTECTED, ACC_SPEC_PUBLIC, ACC_SPEC_SAFE_MATH, ACC_UNINITIALIZED, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_BIGINT_MATH, EVERYTHING, JML_JMLObjectSet, NOT_SPECIFIED, NOTHING, OPE_BACKWARD_IMPLIES, OPE_EQUIV, OPE_EXISTS, OPE_FORALL, OPE_IMPLIES, OPE_L_ARROW, OPE_MAX, OPE_MIN, OPE_NOT_EQUIV, OPE_NUM_OF, OPE_PRODUCT, OPE_R_ARROW, OPE_SUBTYPE, OPE_SUM, SAME, TID_BIGINT, TID_REAL, TID_TYPE, TN_JMLOBJECTSET, TN_JMLTYPE, TN_JMLVALUESET
 
Fields inherited from interface org.multijava.mjc.Constants
ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP
 
Fields inherited from interface org.multijava.util.classfile.Constants
ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID
 
Constructor Summary
private JmlConstructorDeclaration(TokenReference where, JmlMethodSpecification methodSpecification, JConstructorDeclaration delegee)
           
 
Method Summary
 void accept(MjcVisitor p)
          Accepts the specified visitor.
 void acceptDelegee(MjcVisitor p)
           
 boolean hasBody()
          Indicates whether this method declaration has a body.
 boolean isConstructor()
          Returns true if this declaration is for a constructor.
 boolean isExecutableModel()
          Returns true if this constructor is a model constructor and can be executed by simply commenting out annotation markers.
static JmlConstructorDeclaration makeInstance(TokenReference where, long modifiers, String ident, JFormalParameter[] params, CClassType[] exceptions, JConstructorBlock body, JavadocComment javadoc, JavaStyleComment[] comments, JmlMethodSpecification methodSpecification)
           
protected  void resetFinalFieldStatusIfConstructor(CClassContextType context)
          Resets the final field definite assignment info if this is a constructor.
 void typecheck(CClassContextType cContext, CVariableInfoTable instanceInfo)
          Typechecks this method declaration.
 
Methods inherited from class org.jmlspecs.checker.JmlMethodDeclaration
addParameter, body, checkAssignableFields, checkInterface, checkInterfaceType, checkOverriding, checkRefinementConsistency, combineSpecifications, compareTo, createSelfContext, findDeclWithBody, genCode, getAssignableFieldSet, getCombinedSpecification, getExceptions, getMinAssignableFieldSet, hasSpecification, ident, isAbstract, isExternal, isFinalizer, isHelper, isModel, isNative, isOverriding, isPrivate, isPublic, isRacMethod, isSpecProtected, isSpecPublic, isStatic, jmlAccess, jmlchecks, makeInstance, methodSpecification, modifiers, modifiers2, overriddenMethods, parameters, resolveExtMethods, resolveSpecializers, resolveTopMethods, returnType, setBody, setIdent, setModifiers, setModifiers2, setParameters, setRefinementLinks, setRefiningMethod, setSpecstoCombinedSpecs, stringRepresentation, typecheck, usesMultipleDispatch
 
Methods inherited from class org.jmlspecs.checker.JmlMemberDeclaration
checkRefinedModifiers, findJavaFileInRefinement, genComments, getCClass, getCombinedVarAssertions, getField, getMethod, getMostRefined, getRefinedMember, getRefiningMember, inBinaryClassFile, inJavaFile, inners, isDeprecated, isRefined, isRefiningMember, javadocComment, setRefinedMember, setRefiningMember
 
Methods inherited from class org.jmlspecs.checker.JmlNode
enterSpecScope, enterSpecScope, exitSpecScope, exitSpecScope, privacy, privacyString
 
Methods inherited from class org.multijava.mjc.JPhylum
check, check, check, check, fail, fail, fail, warn, warn, warn, warn
 
Methods inherited from class org.multijava.util.compiler.Phylum
getTokenReference, setTokenReference
 
Methods inherited from class org.multijava.util.Utils
assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 
Methods inherited from interface org.multijava.mjc.JMethodDeclarationType
addParameter, body, checkInterface, checkInterfaceType, checkOverriding, compareTo, createSelfContext, getExceptions, ident, isExternal, isOverriding, modifiers, overriddenMethods, parameters, resolveExtMethods, resolveSpecializers, resolveTopMethods, returnType, setModifiers, setParameters, typecheck, usesMultipleDispatch
 
Methods inherited from interface org.multijava.mjc.JMemberDeclarationType
genComments, getCClass, getField, getMethod, isDeprecated
 
Methods inherited from interface org.multijava.util.compiler.PhylumType
getTokenReference, setTokenReference
 
Methods inherited from interface org.multijava.javadoc.Annotatable
javadocComment
 

Field Detail

delegee

private JConstructorDeclaration delegee

instanceInfo

private CVariableInfoTable instanceInfo
Temporarily stores the final field definite assignment information while typechecking the constructor.

Constructor Detail

JmlConstructorDeclaration

private JmlConstructorDeclaration(TokenReference where,
                                  JmlMethodSpecification methodSpecification,
                                  JConstructorDeclaration delegee)
Method Detail

makeInstance

public static JmlConstructorDeclaration makeInstance(TokenReference where,
                                                     long modifiers,
                                                     String ident,
                                                     JFormalParameter[] params,
                                                     CClassType[] exceptions,
                                                     JConstructorBlock body,
                                                     JavadocComment javadoc,
                                                     JavaStyleComment[] comments,
                                                     JmlMethodSpecification methodSpecification)

hasBody

public boolean hasBody()
Description copied from class: JmlMethodDeclaration
Indicates whether this method declaration has a body.

Specified by:
hasBody in interface JMethodDeclarationType
Overrides:
hasBody in class JmlMethodDeclaration

isConstructor

public boolean isConstructor()
Returns true if this declaration is for a constructor.

Overrides:
isConstructor in class JmlMethodDeclaration

isExecutableModel

public boolean isExecutableModel()
Returns true if this constructor is a model constructor and can be executed by simply commenting out annotation markers. This method must be called after typechecking.

Overrides:
isExecutableModel in class JmlMethodDeclaration

accept

public void accept(MjcVisitor p)
Accepts the specified visitor.

Specified by:
accept in interface JMemberDeclarationType
Overrides:
accept in class JmlMethodDeclaration
Parameters:
p - the visitor

acceptDelegee

public void acceptDelegee(MjcVisitor p)
Overrides:
acceptDelegee in class JmlMethodDeclaration

typecheck

public void typecheck(CClassContextType cContext,
                      CVariableInfoTable instanceInfo)
               throws PositionedError
Typechecks this method declaration. Mutates the context to record the information gathered during the checks.

Specified by:
typecheck in interface JConstructorDeclarationType
Parameters:
cContext - the context in which this method appears
instanceInfo - the definite-assignment state of the surrounding class after instance initializers but before any constructors
Throws:
PositionedError - if the checks fail and the failure cannot be recovered from

resetFinalFieldStatusIfConstructor

protected void resetFinalFieldStatusIfConstructor(CClassContextType context)
Resets the final field definite assignment info if this is a constructor.

Overrides:
resetFinalFieldStatusIfConstructor in class JmlMethodDeclaration
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.