JML

org.jmlspecs.jmlrac
Class TransExpression2

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.checker.JmlAbstractVisitor
          extended byorg.jmlspecs.jmlrac.RacAbstractVisitor
              extended byorg.jmlspecs.jmlrac.AbstractExpressionTranslator
                  extended byorg.jmlspecs.jmlrac.TransExpression2
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor, RacConstants, RacVisitor
Direct Known Subclasses:
TransPostExpression2

public class TransExpression2
extends AbstractExpressionTranslator

A RAC visitor class to translate JML expressions into Java source code.

Version:
$Revision: 1.24 $
Author:
Frederic Rioux (based on Yoonsik Cheon's work)

Field Summary
protected  RacContext context
          Current translation context.
protected  String errorType
           
protected  String evaluatorPDef
           
protected  String evaluatorPUse
           
protected  JExpression expression
          Expression to translate.
protected  boolean isInner
          Keep track of this translator is helping a translator translate an inner class
protected  Stack prebuiltStatementsStack
          Contains node that were translated using helpers.
private  boolean properlyEvaluated
           
protected  PositionnedExpressionException reportedException
           
private  String resultingExpression
          String containing visitor methods results.
protected  String resultVar
          Variable to hold the reslt of the target expression.
protected  String thisIs
           
private  boolean translated
          Is the expression already translated?
protected  JTypeDeclarationType typeDecl
          The type declaration within which this expression resides (the type of 'this').
protected  VarGenerator varGen
          Generator of unique variable names.
 
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_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_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, 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, NULLITY_MODS, 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_SYNTHETIC, 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
 
Fields inherited from interface org.jmlspecs.jmlrac.RacConstants
MN_CHECK_HC, MN_CHECK_INV, MN_CHECK_POST, MN_CHECK_PRE, MN_CHECK_XPOST, MN_EVAL_OLD, MN_GHOST, MN_INIT, MN_INTERNAL, MN_MODEL, MN_MODEL_PUBLIC, MN_RESTORE_FROM, MN_SAVE_TO, MN_SPEC, MN_SPEC_PUBLIC, TN_JMLCHECKABLE, TN_JMLSURROGATE, TN_JMLUNIT_TEST_POSTFIX, TN_JMLUNIT_TESTDATA_POSTFIX, TN_JMLVALUE, TN_SURROGATE, VN_ASSERTION, VN_CATCH_VAR, VN_CLASS_INIT, VN_CONSTRUCTED, VN_DELEGEE, VN_ERROR_SET, VN_EXCEPTION, VN_FREE_VAR, VN_INIT, VN_OLD_VAR, VN_POST_VAR, VN_PRE_VAR, VN_PRECOND, VN_RAC_COMPILED, VN_RAC_LEVEL, VN_RESULT, VN_STACK_VAR, VN_XRESULT
 
Constructor Summary
TransExpression2(VarGenerator varGen, RacContext ctx, JExpression expr, String resultVar, JTypeDeclarationType typeDecl, String errorType)
          Constructs an instance and translates the given expression.
 
Method Summary
 RacNode addPrebuiltNode(RacNode initial)
           
static boolean canMakeStaticCall(JClassFieldExpression expr, String receiver)
          Returns true if a static (non-dynamic) call can be made to the given field expression, expr.
protected  void generateBinaryExpression(String oper, String left, String right)
          Generates a binary expression.
protected  void generateTertiaryExpression(String condition, String left, String right)
          Generates a tertiary (conditional) expression.
 String GET_RESULT()
          Returns the top element of the result stack.
protected  void handleExceptionalTranslation(PositionnedExpressionException e)
           
 boolean hasPrebuiltNodes()
           
protected  boolean isNonExecutableFieldReference(JClassFieldExpression expr)
          Returns true if the referenced field (by the argument expression) is not executable.
 boolean isProperlyEvaluated()
           
private static boolean isStatic(JClassFieldExpression expr)
          Returns true if the given field expression refers to a static field.
private static boolean isStatic(JMethodCallExpression expr)
          Returns true if the given method call expression refers to a static method.
protected  void LOG(String str)
          Used for debugging pruposes only.
private  void needDynamicInvocationMethod()
          Records that we need to generate the dynamic invocation method.
protected static void notExecutableClauseWarn(TokenReference tok, String description)
           
protected static void notImplementedClauseFail(TokenReference tok, String description)
           
protected static void notSupportedClauseFail(TokenReference tok, String description)
           
protected  void perform()
          Translates the current expression into a sequence of Java statements that evaluate and store the result in the result variable.
private  String receiverForDynamicCall(JExpression expr)
          Returns the receiver for executing the given expression, expr using a dynamic call.
protected  void RETURN_RESULT(String str)
          Puts the given object to the result stack.
 void setEvaluatorPDef(String str)
           
 void setEvaluatorPUse(String str)
           
static boolean specAccessorNeeded(long modifiers)
          Returns true if the modifiers indicate that we need to generate specification-only accessor method.
 RacNode stmt(boolean wrapped)
          Returns the result of translating the expression.
protected  String stmtAsString()
           
private  String transFieldReference(JClassFieldExpression self, String accPrefix)
          Translates a class field expression that references a model, ghost, spec_public, or spec_protected field.
private  String translatePrimitive(CType type)
           
protected  void translateSpecQuantifiedExpression(TransExpression2 t, JmlSpecQuantifiedExpression self)
           
private  void translateToDynamicCall(JMethodCallExpression expr, boolean isModel)
           
private  void translateToDynamicNewObjectExpression(JNewObjectExpression expr, boolean isSpecPublic)
          Translates the given model, spec_public, or spec_protected constructor call expression, expr, which was determined to be executed using a dynamic call.
private  void translateToStaticCall(JMethodCallExpression self, long kind)
           
private  void translateToStaticNewObjectExpression(JNewObjectExpression self, boolean isSpecPublic)
          Translates the given new object expression into a static call.
 void visitAddExpression(JAddExpression self)
          Translates an add expression.
 void visitArrayAccessExpression(JArrayAccessExpression self)
          Translates a Java array access expression.
 void visitArrayDimsAndInit(JArrayDimsAndInits self)
          visits an array dimension and initialization expression
 void visitArrayInitializer(JArrayInitializer self)
          visits an array initializer expression
 void visitArrayLengthExpression(JArrayLengthExpression self)
          Translates a Java array length expression.
 void visitAssignmentExpression(JAssignmentExpression self)
          Translates a Java assignment expression.
protected  void visitBigintLiteral(long value)
          Translates a \bigint literal.
protected  void visitBinaryExpression(JBinaryExpression self, String oper)
          Translates various types of supported binary expression into left opr ritgh.
 void visitBitwiseExpression(JBitwiseExpression self)
          Translates a bitwise expression into left opr ritgh.
 void visitBooleanLiteral(JBooleanLiteral self)
          Translates a boolean literal.
protected  void visitByteLiteral(byte value)
          Translates a byte literal.
 void visitCastExpression(JCastExpression self)
          Translates a cast expression.
 void visitCharLiteral(JCharLiteral self)
          Translates a character literal.
 void visitClassExpression(JClassExpression self)
          Translates a Java class expression.
 void visitCompoundAssignmentExpression(JAssignmentExpression self)
          Translates a Java compound assignment expression.
 void visitConditionalAndExpression(JConditionalAndExpression self)
          Translates a conditional "and" expression into left && right.
 void visitConditionalExpression(JConditionalExpression self)
          Translates a conditional expression.
 void visitConditionalOrExpression(JConditionalOrExpression self)
          Translates a conditional "or" expression into left || right.
 void visitDivideExpression(JDivideExpression self)
          Translates a divide expression.
protected  void visitDoubleLiteral(double value)
          Translates a double literal.
 void visitEqualityExpression(JEqualityExpression self)
          Translates an equality expression into left opr right.
 void visitExplicitConstructorInvocation(JExplicitConstructorInvocation self)
          Translates an explicit constructor invocation
 void visitFieldExpression(JClassFieldExpression self)
          Translates a Java field expression.
protected  void visitFloatLiteral(float value)
          Translates a float literal.
 void visitInstanceofExpression(JInstanceofExpression self)
          Translates a Java instanceof expression.
protected  void visitIntLiteral(int value)
          Translates a int literal.
 void visitJmlElemTypeExpression(JmlElemTypeExpression self)
          Translated a JmlElemTypeExpression.
 void visitJmlFreshExpression(JmlFreshExpression self)
          Translates a JmlFreshExpression expression.
 void visitJmlInformalExpression(JmlInformalExpression self)
          Translates a JmlInformalExpression expression.
 void visitJmlInvariantForExpression(JmlInvariantForExpression self)
          NOT SUPPORTED The \invariant_for operator returns true just when its argument satisfies the invariant of its static type.
 void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
           
 void visitJmlLabelExpression(JmlLabelExpression self)
           
 void visitJmlLockSetExpression(JmlLockSetExpression self)
           
 void visitJmlMaxExpression(JmlMaxExpression self)
           
 void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
          NOT SUPPORTED Translates a JmlNonNullElementsExpression.
 void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
          Translates a JmlNotAssignedExpression expression.
 void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
          Translates a JmlNotModifiedExpression expression.
 void visitJmlOldExpression(JmlOldExpression self)
           
 void visitJmlPredicate(JmlPredicate self)
          Translates the given JML predicate.
 void visitJmlPreExpression(JmlPreExpression self)
           
 void visitJmlReachExpression(JmlReachExpression self)
           
 void visitJmlRelationalExpression(JmlRelationalExpression self)
          Translates a JML relational expression.
 void visitJmlResultExpression(JmlResultExpression self)
           
 void visitJmlSetComprehension(JmlSetComprehension self)
           
 void visitJmlSpecExpression(JmlSpecExpression self)
          Translates the given JML spec expression.
 void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
           
 void visitJmlTypeExpression(JmlTypeExpression self)
          Translated a JmlTypeExpression.
 void visitJmlTypeOfExpression(JmlTypeOfExpression self)
          Translated a JmlTypeExpression.
 void visitLocalVariableExpression(JLocalVariableExpression self)
          Translates a Java local variable expression.
protected  void visitLongLiteral(long value)
          Translates a long literal.
 void visitMethodCallExpression(JMethodCallExpression self)
          Translates a Java method call expression.
 void visitMinusExpression(JMinusExpression self)
          Translates a minus expression.
 void visitModuloExpression(JModuloExpression self)
          Translates a modulo division expression.
 void visitMultExpression(JMultExpression self)
          Translates a multiplication expression.
 void visitNameExpression(JNameExpression self)
          Translates a Java name expression.
 void visitNewAnonymousClassExpression(JNewAnonymousClassExpression self)
          Translates an object allocator expression for an anonymous class.
 void visitNewArrayExpression(JNewArrayExpression self)
          Translates an array allocator expression.
 void visitNewObjectExpression(JNewObjectExpression self)
          Translates a Java new object expression.
 void visitNullLiteral(JNullLiteral self)
          Translates a null literal.
 void visitOrdinalLiteral(JOrdinalLiteral self)
          Translates an ordinal literal.
 void visitParenthesedExpression(JParenthesedExpression self)
          Translates a JParenthesedExpression expression into ( expr ).
 void visitPostfixExpression(JPostfixExpression self)
          Translates a Java postfix expression.
 void visitPrefixExpression(JPrefixExpression self)
          Translates a Java prefix expression.
 void visitRacPredicate(RacPredicate self)
          Translates the given RAC predicate.
 void visitRealLiteral(JRealLiteral self)
          Translates a real literal.
 void visitRelationalExpression(JRelationalExpression self)
          Translates java relational expression.
 void visitShiftExpression(JShiftExpression self)
          Translates a shift expression.
protected  void visitShortLiteral(short value)
          Translates a short literal.
 void visitStringLiteral(JStringLiteral self)
          Translates a string literal.
 void visitSuperExpression(JSuperExpression self)
          visits a super expression
 void visitThisExpression(JThisExpression self)
          visits a this expression
 void visitTypeNameExpression(JTypeNameExpression self)
          Translates a Java type name expression
 void visitUnaryExpression(JUnaryExpression self)
          Translates a JUnaryExpression expression into opr expr.
 void visitUnaryPromoteExpression(JUnaryPromote self)
          Translates a Java unary promotion expression.
protected  RacNode wrap(RacNode node)
           
 
Methods inherited from class org.jmlspecs.jmlrac.RacAbstractVisitor
visitRacNode
 
Methods inherited from class org.jmlspecs.checker.JmlAbstractVisitor
visitAssertStatement, visitBlockStatement, visitBreakStatement, visitCatchClause, visitClassBlock, visitClassDeclaration, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitCompoundStatement, visitCompoundStatement, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDoStatement, visitEmptyStatement, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInterfaceDeclaration, visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBehaviorSpec, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalBehaviorSpec, visitJmlExceptionalExample, visitJmlExceptionalSpecBody, visitJmlExceptionalSpecCase, visitJmlExpression, visitJmlExtendingSpecification, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlGeneralSpecCase, visitJmlGenericSpecBody, visitJmlGenericSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantStatement, visitJmlLetVarDecl, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNormalBehaviorSpec, visitJmlNormalExample, visitJmlNormalSpecBody, visitJmlNormalSpecCase, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicateKeyword, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlReturnsClause, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecification, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion, visitLabeledStatement, visitMathModeExpression, visitMethodDeclaration, visitPackageImport, visitPackageName, visitReturnStatement, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement
 
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.jmlspecs.checker.JmlVisitor
visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBehaviorSpec, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalBehaviorSpec, visitJmlExceptionalExample, visitJmlExceptionalSpecBody, visitJmlExceptionalSpecCase, visitJmlExpression, visitJmlExtendingSpecification, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlGeneralSpecCase, visitJmlGenericSpecBody, visitJmlGenericSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantStatement, visitJmlLetVarDecl, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNormalBehaviorSpec, visitJmlNormalExample, visitJmlNormalSpecBody, visitJmlNormalSpecCase, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicateKeyword, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlReturnsClause, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecification, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion
 
Methods inherited from interface org.multijava.mjc.MjcVisitor
visitAssertStatement, visitBlockStatement, visitBreakStatement, visitCatchClause, visitClassBlock, visitClassDeclaration, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitCompoundStatement, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDoStatement, visitEmptyStatement, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInterfaceDeclaration, visitLabeledStatement, visitMathModeExpression, visitMethodDeclaration, visitPackageImport, visitPackageName, visitReturnStatement, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement
 

Field Detail

varGen

protected VarGenerator varGen
Generator of unique variable names.


resultVar

protected String resultVar
Variable to hold the reslt of the target expression.


resultingExpression

private String resultingExpression
String containing visitor methods results.


context

protected RacContext context
Current translation context.


expression

protected JExpression expression
Expression to translate.


typeDecl

protected JTypeDeclarationType typeDecl
The type declaration within which this expression resides (the type of 'this').


translated

private boolean translated
Is the expression already translated?


errorType

protected String errorType

properlyEvaluated

private boolean properlyEvaluated

reportedException

protected PositionnedExpressionException reportedException

isInner

protected boolean isInner
Keep track of this translator is helping a translator translate an inner class


prebuiltStatementsStack

protected Stack prebuiltStatementsStack
Contains node that were translated using helpers. They are to be appended before the actual expressions's translation


evaluatorPUse

protected String evaluatorPUse

evaluatorPDef

protected String evaluatorPDef

thisIs

protected String thisIs
Constructor Detail

TransExpression2

public TransExpression2(VarGenerator varGen,
                        RacContext ctx,
                        JExpression expr,
                        String resultVar,
                        JTypeDeclarationType typeDecl,
                        String errorType)
Constructs an instance and translates the given expression.

Parameters:
varGen - variable generator to be used for generating fresh variable names necessary in the translated code.
expr - expression to be translated.
resultVar - variable to store the result. In the translated code, the result of the expression is stored in the variable whose name given by this parameter.
Method Detail

stmt

public RacNode stmt(boolean wrapped)
Returns the result of translating the expression.

Returns:
translation result

stmtAsString

protected String stmtAsString()

wrap

protected RacNode wrap(RacNode node)

addPrebuiltNode

public RacNode addPrebuiltNode(RacNode initial)

hasPrebuiltNodes

public boolean hasPrebuiltNodes()

perform

protected void perform()
Translates the current expression into a sequence of Java statements that evaluate and store the result in the result variable. The result variable is assumed to be declared in the outer scope.


handleExceptionalTranslation

protected void handleExceptionalTranslation(PositionnedExpressionException e)

visitRacPredicate

public void visitRacPredicate(RacPredicate self)
Translates the given RAC predicate.

Specified by:
visitRacPredicate in interface RacVisitor
Overrides:
visitRacPredicate in class RacAbstractVisitor

visitJmlPredicate

public void visitJmlPredicate(JmlPredicate self)
Translates the given JML predicate.

Specified by:
visitJmlPredicate in interface JmlVisitor
Overrides:
visitJmlPredicate in class JmlAbstractVisitor

visitJmlSpecExpression

public void visitJmlSpecExpression(JmlSpecExpression self)
Translates the given JML spec expression.

Specified by:
visitJmlSpecExpression in interface JmlVisitor
Overrides:
visitJmlSpecExpression in class JmlAbstractVisitor

visitJmlNonNullElementsExpression

public void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
NOT SUPPORTED Translates a JmlNonNullElementsExpression. The operator \nonnullelements can be used to assert that an array and its elements are all non-null True is the array is not null and all of its elements are non-null. False otherwise.

Specified by:
visitJmlNonNullElementsExpression in interface JmlVisitor
Overrides:
visitJmlNonNullElementsExpression in class JmlAbstractVisitor

visitJmlElemTypeExpression

public void visitJmlElemTypeExpression(JmlElemTypeExpression self)
Translated a JmlElemTypeExpression. The \elemtype operator returns the most-specific static type shared by all elements of its array argument

Specified by:
visitJmlElemTypeExpression in interface JmlVisitor
Overrides:
visitJmlElemTypeExpression in class JmlAbstractVisitor

visitJmlNotModifiedExpression

public void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
Translates a JmlNotModifiedExpression expression. (Not executable)

Specified by:
visitJmlNotModifiedExpression in interface JmlVisitor
Overrides:
visitJmlNotModifiedExpression in class JmlAbstractVisitor

visitJmlNotAssignedExpression

public void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
Translates a JmlNotAssignedExpression expression. (Not executable)

Specified by:
visitJmlNotAssignedExpression in interface JmlVisitor
Overrides:
visitJmlNotAssignedExpression in class JmlAbstractVisitor

visitJmlFreshExpression

public void visitJmlFreshExpression(JmlFreshExpression self)
Translates a JmlFreshExpression expression. (Not executable)

Specified by:
visitJmlFreshExpression in interface JmlVisitor
Overrides:
visitJmlFreshExpression in class JmlAbstractVisitor

visitJmlInformalExpression

public void visitJmlInformalExpression(JmlInformalExpression self)
Translates a JmlInformalExpression expression. (Not executable)

Specified by:
visitJmlInformalExpression in interface JmlVisitor
Overrides:
visitJmlInformalExpression in class JmlAbstractVisitor

visitJmlInvariantForExpression

public void visitJmlInvariantForExpression(JmlInvariantForExpression self)
NOT SUPPORTED The \invariant_for operator returns true just when its argument satisfies the invariant of its static type.

Specified by:
visitJmlInvariantForExpression in interface JmlVisitor
Overrides:
visitJmlInvariantForExpression in class JmlAbstractVisitor

visitJmlIsInitializedExpression

public void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
Specified by:
visitJmlIsInitializedExpression in interface JmlVisitor
Overrides:
visitJmlIsInitializedExpression in class JmlAbstractVisitor

visitJmlLabelExpression

public void visitJmlLabelExpression(JmlLabelExpression self)
Specified by:
visitJmlLabelExpression in interface JmlVisitor
Overrides:
visitJmlLabelExpression in class JmlAbstractVisitor

visitJmlLockSetExpression

public void visitJmlLockSetExpression(JmlLockSetExpression self)
Specified by:
visitJmlLockSetExpression in interface JmlVisitor
Overrides:
visitJmlLockSetExpression in class JmlAbstractVisitor

visitJmlOldExpression

public void visitJmlOldExpression(JmlOldExpression self)
Specified by:
visitJmlOldExpression in interface JmlVisitor
Overrides:
visitJmlOldExpression in class JmlAbstractVisitor

visitJmlPreExpression

public void visitJmlPreExpression(JmlPreExpression self)
Specified by:
visitJmlPreExpression in interface JmlVisitor
Overrides:
visitJmlPreExpression in class JmlAbstractVisitor

visitJmlReachExpression

public void visitJmlReachExpression(JmlReachExpression self)
Specified by:
visitJmlReachExpression in interface JmlVisitor
Overrides:
visitJmlReachExpression in class JmlAbstractVisitor

visitJmlResultExpression

public void visitJmlResultExpression(JmlResultExpression self)
Specified by:
visitJmlResultExpression in interface JmlVisitor
Overrides:
visitJmlResultExpression in class JmlAbstractVisitor

visitJmlSetComprehension

public void visitJmlSetComprehension(JmlSetComprehension self)
Specified by:
visitJmlSetComprehension in interface JmlVisitor
Overrides:
visitJmlSetComprehension in class JmlAbstractVisitor

visitJmlSpecQuantifiedExpression

public void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
Specified by:
visitJmlSpecQuantifiedExpression in interface JmlVisitor
Overrides:
visitJmlSpecQuantifiedExpression in class JmlAbstractVisitor

translateSpecQuantifiedExpression

protected void translateSpecQuantifiedExpression(TransExpression2 t,
                                                 JmlSpecQuantifiedExpression self)

visitJmlTypeExpression

public void visitJmlTypeExpression(JmlTypeExpression self)
Translated a JmlTypeExpression. The operator \type can be used to mark types in expressions.

Specified by:
visitJmlTypeExpression in interface JmlVisitor
Overrides:
visitJmlTypeExpression in class JmlAbstractVisitor

visitJmlTypeOfExpression

public void visitJmlTypeOfExpression(JmlTypeOfExpression self)
Translated a JmlTypeExpression. The operator \typeof returns the most-specific dynamic type of an expression's value.

Specified by:
visitJmlTypeOfExpression in interface JmlVisitor
Overrides:
visitJmlTypeOfExpression in class JmlAbstractVisitor

translatePrimitive

private String translatePrimitive(CType type)

visitJmlMaxExpression

public void visitJmlMaxExpression(JmlMaxExpression self)
Specified by:
visitJmlMaxExpression in interface JmlVisitor
Overrides:
visitJmlMaxExpression in class JmlAbstractVisitor

visitAssignmentExpression

public void visitAssignmentExpression(JAssignmentExpression self)
Translates a Java assignment expression. The JML type checker gurantees that this be never visited, i.e., assignment expressions are not allowed in JML expression.

Specified by:
visitAssignmentExpression in interface MjcVisitor
Overrides:
visitAssignmentExpression in class JmlAbstractVisitor

visitCompoundAssignmentExpression

public void visitCompoundAssignmentExpression(JAssignmentExpression self)
Translates a Java compound assignment expression. The JML type checker gurantees that this be never visited, i.e., assignment expressions are not allowed in JML expression.


visitBinaryExpression

protected void visitBinaryExpression(JBinaryExpression self,
                                     String oper)
Translates various types of supported binary expression into left opr ritgh. -JBinaryArithmeticExpression -- JAddExpression (+) -- JBitwiseExpression (&, |, ^) -- JDivideExpression (/) -- JMinusExpression (-) -- JModuloExpression (%) -- JMultExpression (*) -- JShiftExpression (<<, >>, >>>) - JConditionalAndExpression (&&) - JConditionalOrExpression (||) - JEqualityExpression (==, !=) - JRelationalExpression (<, <=, >, >=)

Overrides:
visitBinaryExpression in class JmlAbstractVisitor

generateBinaryExpression

protected void generateBinaryExpression(String oper,
                                        String left,
                                        String right)
Generates a binary expression.


visitEqualityExpression

public void visitEqualityExpression(JEqualityExpression self)
Translates an equality expression into left opr right.

Specified by:
visitEqualityExpression in interface MjcVisitor
Overrides:
visitEqualityExpression in class JmlAbstractVisitor

visitConditionalAndExpression

public void visitConditionalAndExpression(JConditionalAndExpression self)
Translates a conditional "and" expression into left && right.

Specified by:
visitConditionalAndExpression in interface MjcVisitor
Overrides:
visitConditionalAndExpression in class JmlAbstractVisitor

visitConditionalOrExpression

public void visitConditionalOrExpression(JConditionalOrExpression self)
Translates a conditional "or" expression into left || right.

Specified by:
visitConditionalOrExpression in interface MjcVisitor
Overrides:
visitConditionalOrExpression in class JmlAbstractVisitor

visitBitwiseExpression

public void visitBitwiseExpression(JBitwiseExpression self)
Translates a bitwise expression into left opr ritgh.

Specified by:
visitBitwiseExpression in interface MjcVisitor
Overrides:
visitBitwiseExpression in class JmlAbstractVisitor

visitAddExpression

public void visitAddExpression(JAddExpression self)
Translates an add expression.

Specified by:
visitAddExpression in interface MjcVisitor
Overrides:
visitAddExpression in class JmlAbstractVisitor

visitMinusExpression

public void visitMinusExpression(JMinusExpression self)
Translates a minus expression.

Specified by:
visitMinusExpression in interface MjcVisitor
Overrides:
visitMinusExpression in class JmlAbstractVisitor

visitMultExpression

public void visitMultExpression(JMultExpression self)
Translates a multiplication expression.

Specified by:
visitMultExpression in interface MjcVisitor
Overrides:
visitMultExpression in class JmlAbstractVisitor

visitDivideExpression

public void visitDivideExpression(JDivideExpression self)
Translates a divide expression.

Specified by:
visitDivideExpression in interface MjcVisitor
Overrides:
visitDivideExpression in class JmlAbstractVisitor

visitModuloExpression

public void visitModuloExpression(JModuloExpression self)
Translates a modulo division expression.

Specified by:
visitModuloExpression in interface MjcVisitor
Overrides:
visitModuloExpression in class JmlAbstractVisitor

visitShiftExpression

public void visitShiftExpression(JShiftExpression self)
Translates a shift expression.

Specified by:
visitShiftExpression in interface MjcVisitor
Overrides:
visitShiftExpression in class JmlAbstractVisitor

visitRelationalExpression

public void visitRelationalExpression(JRelationalExpression self)
Translates java relational expression.

Specified by:
visitRelationalExpression in interface MjcVisitor
Overrides:
visitRelationalExpression in class JmlAbstractVisitor

visitJmlRelationalExpression

public void visitJmlRelationalExpression(JmlRelationalExpression self)
Translates a JML relational expression.

Specified by:
visitJmlRelationalExpression in interface JmlVisitor
Overrides:
visitJmlRelationalExpression in class JmlAbstractVisitor

generateTertiaryExpression

protected void generateTertiaryExpression(String condition,
                                          String left,
                                          String right)
Generates a tertiary (conditional) expression.


visitConditionalExpression

public void visitConditionalExpression(JConditionalExpression self)
Translates a conditional expression.

Specified by:
visitConditionalExpression in interface MjcVisitor
Overrides:
visitConditionalExpression in class JmlAbstractVisitor

visitCastExpression

public void visitCastExpression(JCastExpression self)
Translates a cast expression.

Specified by:
visitCastExpression in interface MjcVisitor
Overrides:
visitCastExpression in class JmlAbstractVisitor

visitUnaryPromoteExpression

public void visitUnaryPromoteExpression(JUnaryPromote self)
Translates a Java unary promotion expression.

Specified by:
visitUnaryPromoteExpression in interface MjcVisitor
Overrides:
visitUnaryPromoteExpression in class JmlAbstractVisitor

visitUnaryExpression

public void visitUnaryExpression(JUnaryExpression self)
Translates a JUnaryExpression expression into opr expr.

Specified by:
visitUnaryExpression in interface MjcVisitor
Overrides:
visitUnaryExpression in class JmlAbstractVisitor

visitParenthesedExpression

public void visitParenthesedExpression(JParenthesedExpression self)
Translates a JParenthesedExpression expression into ( expr ).

Specified by:
visitParenthesedExpression in interface MjcVisitor
Overrides:
visitParenthesedExpression in class JmlAbstractVisitor

visitInstanceofExpression

public void visitInstanceofExpression(JInstanceofExpression self)
Translates a Java instanceof expression.

Specified by:
visitInstanceofExpression in interface MjcVisitor
Overrides:
visitInstanceofExpression in class JmlAbstractVisitor

visitLocalVariableExpression

public void visitLocalVariableExpression(JLocalVariableExpression self)
Translates a Java local variable expression.

Specified by:
visitLocalVariableExpression in interface MjcVisitor
Overrides:
visitLocalVariableExpression in class JmlAbstractVisitor

visitFieldExpression

public void visitFieldExpression(JClassFieldExpression self)
Translates a Java field expression.

Specified by:
visitFieldExpression in interface MjcVisitor
Overrides:
visitFieldExpression in class JmlAbstractVisitor

isNonExecutableFieldReference

protected boolean isNonExecutableFieldReference(JClassFieldExpression expr)
Returns true if the referenced field (by the argument expression) is not executable. If the referenced field is declared inside a model class or interface, it is not executable. A model/ghost field declared in a non-model class/interface is executable, e.g., by calling its access method.


specAccessorNeeded

public static boolean specAccessorNeeded(long modifiers)
Returns true if the modifiers indicate that we need to generate specification-only accessor method. The argument modifier is typically from a model field declaration.

 ensures \result == (hasFlag(modifiers, ACC_PRIVATE) &&
	    (hasFlag(modifiers, ACC_SPEC_PUBLIC) ||
	     hasFlag(modifiers, ACC_SPEC_PROTECTED)));
 


transFieldReference

private String transFieldReference(JClassFieldExpression self,
                                   String accPrefix)
Translates a class field expression that references a model, ghost, spec_public, or spec_protected field. The translated code dynamically invokes the corresponding accessor method.


receiverForDynamicCall

private String receiverForDynamicCall(JExpression expr)
Returns the receiver for executing the given expression, expr using a dynamic call. The argument is supposed to be either a non-static JClassFieldExpression referring to a model, ghost, spec_public, or spec_protected field or a non-static JMethodCallExpression calling a spec_public or spec_protected method. If the receiver is "this", a null value is returned; otherwise, the returned source code, if executed, evaluates the receiver and assign it to the fresh variable whose name is given by the name field of RacNode.


needDynamicInvocationMethod

private void needDynamicInvocationMethod()
Records that we need to generate the dynamic invocation method. E.g., to evaluate model, ghost, spec_public, or spec_protected fields or spec_public or spec_protected methods.


canMakeStaticCall

public static boolean canMakeStaticCall(JClassFieldExpression expr,
                                        String receiver)
Returns true if a static (non-dynamic) call can be made to the given field expression, expr. The given expression is assumed to be a reference to a model, ghost, spec_public, or spec_protected field.


isStatic

private static boolean isStatic(JClassFieldExpression expr)
Returns true if the given field expression refers to a static field.


isStatic

private static boolean isStatic(JMethodCallExpression expr)
Returns true if the given method call expression refers to a static method.


visitMethodCallExpression

public void visitMethodCallExpression(JMethodCallExpression self)
Translates a Java method call expression.

Specified by:
visitMethodCallExpression in interface MjcVisitor
Overrides:
visitMethodCallExpression in class JmlAbstractVisitor

translateToStaticCall

private void translateToStaticCall(JMethodCallExpression self,
                                   long kind)

translateToDynamicCall

private void translateToDynamicCall(JMethodCallExpression expr,
                                    boolean isModel)

visitThisExpression

public void visitThisExpression(JThisExpression self)
Description copied from interface: MjcVisitor
visits a this expression

Specified by:
visitThisExpression in interface MjcVisitor
Overrides:
visitThisExpression in class JmlAbstractVisitor

visitSuperExpression

public void visitSuperExpression(JSuperExpression self)
Description copied from interface: MjcVisitor
visits a super expression

Specified by:
visitSuperExpression in interface MjcVisitor
Overrides:
visitSuperExpression in class JmlAbstractVisitor

visitPrefixExpression

public void visitPrefixExpression(JPrefixExpression self)
Translates a Java prefix expression. The JML type checker gurantees that this be never visited, i.e., prefix expressions are not allowed in JML expression.

Specified by:
visitPrefixExpression in interface MjcVisitor
Overrides:
visitPrefixExpression in class JmlAbstractVisitor

visitPostfixExpression

public void visitPostfixExpression(JPostfixExpression self)
Translates a Java postfix expression. The JML type checker gurantees that this be never visited, i.e., postfix expressions are not allowed in JML expression.

Specified by:
visitPostfixExpression in interface MjcVisitor
Overrides:
visitPostfixExpression in class JmlAbstractVisitor

visitTypeNameExpression

public void visitTypeNameExpression(JTypeNameExpression self)
Translates a Java type name expression

Specified by:
visitTypeNameExpression in interface MjcVisitor
Overrides:
visitTypeNameExpression in class JmlAbstractVisitor

visitArrayLengthExpression

public void visitArrayLengthExpression(JArrayLengthExpression self)
Translates a Java array length expression. The translation rules for this expression is defined as follows.

Specified by:
visitArrayLengthExpression in interface MjcVisitor
Overrides:
visitArrayLengthExpression in class JmlAbstractVisitor

visitArrayAccessExpression

public void visitArrayAccessExpression(JArrayAccessExpression self)
Translates a Java array access expression.

Specified by:
visitArrayAccessExpression in interface MjcVisitor
Overrides:
visitArrayAccessExpression in class JmlAbstractVisitor

visitClassExpression

public void visitClassExpression(JClassExpression self)
Translates a Java class expression.

Specified by:
visitClassExpression in interface MjcVisitor
Overrides:
visitClassExpression in class JmlAbstractVisitor

visitExplicitConstructorInvocation

public void visitExplicitConstructorInvocation(JExplicitConstructorInvocation self)
Translates an explicit constructor invocation

Specified by:
visitExplicitConstructorInvocation in interface MjcVisitor
Overrides:
visitExplicitConstructorInvocation in class JmlAbstractVisitor

visitNameExpression

public void visitNameExpression(JNameExpression self)
Translates a Java name expression.

Specified by:
visitNameExpression in interface MjcVisitor
Overrides:
visitNameExpression in class JmlAbstractVisitor

visitNewObjectExpression

public void visitNewObjectExpression(JNewObjectExpression self)
Translates a Java new object expression.

Specified by:
visitNewObjectExpression in interface MjcVisitor
Overrides:
visitNewObjectExpression in class JmlAbstractVisitor

translateToStaticNewObjectExpression

private void translateToStaticNewObjectExpression(JNewObjectExpression self,
                                                  boolean isSpecPublic)
Translates the given new object expression into a static call.


translateToDynamicNewObjectExpression

private void translateToDynamicNewObjectExpression(JNewObjectExpression expr,
                                                   boolean isSpecPublic)
Translates the given model, spec_public, or spec_protected constructor call expression, expr, which was determined to be executed using a dynamic call. If the argument, isSpecPublic, is true, the new expression is for a spec_public or spec_protected constructor; otherwise, it is for a model constructor.


visitNewAnonymousClassExpression

public void visitNewAnonymousClassExpression(JNewAnonymousClassExpression self)
Translates an object allocator expression for an anonymous class.

Specified by:
visitNewAnonymousClassExpression in interface MjcVisitor
Overrides:
visitNewAnonymousClassExpression in class JmlAbstractVisitor

visitNewArrayExpression

public void visitNewArrayExpression(JNewArrayExpression self)
Translates an array allocator expression.

Specified by:
visitNewArrayExpression in interface MjcVisitor
Overrides:
visitNewArrayExpression in class JmlAbstractVisitor

visitArrayDimsAndInit

public void visitArrayDimsAndInit(JArrayDimsAndInits self)
Description copied from interface: MjcVisitor
visits an array dimension and initialization expression

Specified by:
visitArrayDimsAndInit in interface MjcVisitor
Overrides:
visitArrayDimsAndInit in class JmlAbstractVisitor

visitArrayInitializer

public void visitArrayInitializer(JArrayInitializer self)
Description copied from interface: MjcVisitor
visits an array initializer expression

Specified by:
visitArrayInitializer in interface MjcVisitor
Overrides:
visitArrayInitializer in class JmlAbstractVisitor

visitBooleanLiteral

public void visitBooleanLiteral(JBooleanLiteral self)
Translates a boolean literal.

Specified by:
visitBooleanLiteral in interface MjcVisitor
Overrides:
visitBooleanLiteral in class JmlAbstractVisitor

visitCharLiteral

public void visitCharLiteral(JCharLiteral self)
Translates a character literal.

Specified by:
visitCharLiteral in interface MjcVisitor
Overrides:
visitCharLiteral in class JmlAbstractVisitor

visitOrdinalLiteral

public void visitOrdinalLiteral(JOrdinalLiteral self)
Translates an ordinal literal.

Specified by:
visitOrdinalLiteral in interface MjcVisitor
Overrides:
visitOrdinalLiteral in class JmlAbstractVisitor

visitByteLiteral

protected void visitByteLiteral(byte value)
Translates a byte literal.

Overrides:
visitByteLiteral in class JmlAbstractVisitor

visitIntLiteral

protected void visitIntLiteral(int value)
Translates a int literal.

Overrides:
visitIntLiteral in class JmlAbstractVisitor

visitLongLiteral

protected void visitLongLiteral(long value)
Translates a long literal.

Overrides:
visitLongLiteral in class JmlAbstractVisitor

visitBigintLiteral

protected void visitBigintLiteral(long value)
Translates a \bigint literal.


visitShortLiteral

protected void visitShortLiteral(short value)
Translates a short literal.

Overrides:
visitShortLiteral in class JmlAbstractVisitor

visitRealLiteral

public void visitRealLiteral(JRealLiteral self)
Translates a real literal.

Specified by:
visitRealLiteral in interface MjcVisitor
Overrides:
visitRealLiteral in class JmlAbstractVisitor

visitDoubleLiteral

protected void visitDoubleLiteral(double value)
Translates a double literal.

Overrides:
visitDoubleLiteral in class JmlAbstractVisitor

visitFloatLiteral

protected void visitFloatLiteral(float value)
Translates a float literal.

Overrides:
visitFloatLiteral in class JmlAbstractVisitor

visitStringLiteral

public void visitStringLiteral(JStringLiteral self)
Translates a string literal.

Specified by:
visitStringLiteral in interface MjcVisitor
Overrides:
visitStringLiteral in class JmlAbstractVisitor

visitNullLiteral

public void visitNullLiteral(JNullLiteral self)
Translates a null literal.

Specified by:
visitNullLiteral in interface MjcVisitor
Overrides:
visitNullLiteral in class JmlAbstractVisitor

GET_RESULT

public String GET_RESULT()
Returns the top element of the result stack.


RETURN_RESULT

protected void RETURN_RESULT(String str)
Puts the given object to the result stack. I.e., simulates returning of visitor method calls (to the calling visitor method).


LOG

protected void LOG(String str)
Used for debugging pruposes only.


notExecutableClauseWarn

protected static void notExecutableClauseWarn(TokenReference tok,
                                              String description)

notImplementedClauseFail

protected static void notImplementedClauseFail(TokenReference tok,
                                               String description)

notSupportedClauseFail

protected static void notSupportedClauseFail(TokenReference tok,
                                             String description)

isProperlyEvaluated

public boolean isProperlyEvaluated()

setEvaluatorPUse

public void setEvaluatorPUse(String str)

setEvaluatorPDef

public void setEvaluatorPDef(String str)

JML

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.