JML

org.jmlspecs.jmlrac
Class TransExpressionSideEffect

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.TransExpression
                      extended byorg.jmlspecs.jmlrac.TransExpressionSideEffect
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor, RacConstants, RacVisitor

public class TransExpressionSideEffect
extends TransExpression

A special expression translator that allows translation of expressions with side-effects. Several visitor methods are overridden to translate expressions with side-effects, such as assignment expressions, increment expresions, and decrement expressions.

Version:
$Revision: 1.3 $
Author:
Yoonsik Cheon

Nested Class Summary
 
Nested classes inherited from class org.jmlspecs.jmlrac.TransExpression
TransExpression.DiagTerm
 
Field Summary
 
Fields inherited from class org.jmlspecs.jmlrac.TransExpression
context, expression, paramStack, resultStack, resultVar, typeDecl, varGen
 
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
TransExpressionSideEffect(VarGenerator varGen, RacContext ctx, JExpression expr, String resultVar, JTypeDeclarationType typeDecl)
          Constructs an instance and translates the given expression.
TransExpressionSideEffect(VarGenerator varGen, JExpression expr, String resultVar, JTypeDeclarationType typeDecl)
          Constructs an instance and translates the given expression.
 
Method Summary
private  RacNode assignStmt(JExpression expr, String var)
          Generates a statement that assigns the value of var to expr.
private static String operator(int opr)
          Returns the string representation of the desugared increment or decrement operator.
 void transAssignmentExpression(JAssignmentExpression expr)
          Translates the given assignment expresson.
 void visitAssignmentExpression(JAssignmentExpression self)
          Translates the given assignment expression, self.
 void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
          Translates the given compund assignment expression.
 void visitPostfixExpression(JPostfixExpression self)
          Translates the given prefix expression.
 void visitPrefixExpression(JPrefixExpression self)
          Translates the given prefix expression.
 
Methods inherited from class org.jmlspecs.jmlrac.TransExpression
addDiagTerm, addDiagTermResult, addDiagTermThis, applyArrayAccessExpression, applyCast, applyOperator, applyOperator, booleanNonExecutableExpression, canMakeStaticCall, defaultValue, diagTerms, freshVar, GET_ARGUMENT, GET_RESULT, guardUndefined, hasDiagTerms, initDiagTerms, isNonExecutableFieldReference, nonExecutableExpression, PEEK_ARGUMENT, perform, PUT_ARGUMENT, RETURN_RESULT, specAccessorNeeded, stmt, toString, translate, translate, translateEquivalence, translateImplication, translateIsSubtypeOf, transPrefix, transPrefixSpec, visitAddExpression, visitArrayAccessExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitBigintLiteral, visitBinaryExpression, visitBitwiseExpression, visitBooleanBinaryExpression, visitBooleanLiteral, visitByteLiteral, visitCastExpression, visitCharLiteral, visitClassExpression, visitCompoundAssignmentExpression, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitDivideExpression, visitDoubleLiteral, visitEqualityExpression, visitExplicitConstructorInvocation, visitFieldExpression, visitFloatLiteral, visitInstanceofExpression, visitIntLiteral, visitJmlElemTypeExpression, visitJmlFreshExpression, visitJmlInformalExpression, visitJmlInvariantForExpression, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLockSetExpression, visitJmlMaxExpression, visitJmlNonNullElementsExpression, visitJmlNotAssignedExpression, visitJmlNotModifiedExpression, visitJmlOldExpression, visitJmlPredicate, visitJmlPreExpression, visitJmlReachExpression, visitJmlRelationalExpression, visitJmlResultExpression, visitJmlSetComprehension, visitJmlSpecExpression, visitJmlSpecQuantifiedExpression, visitJmlTypeExpression, visitJmlTypeOfExpression, visitLocalVariableExpression, visitLongLiteral, visitMethodCallExpression, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitNewObjectExpression, visitNullLiteral, visitOrdinalLiteral, visitParenthesedExpression, visitRacPredicate, visitRealLiteral, visitRelationalExpression, visitShiftExpression, visitShortLiteral, visitStringLiteral, visitSuperExpression, visitThisExpression, visitTypeNameExpression, visitUnaryExpression, visitUnaryPromoteExpression, warn, wrapBooleanResult, wrapBooleanResultTC, wrappedStmt
 
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, 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, 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
 

Constructor Detail

TransExpressionSideEffect

public TransExpressionSideEffect(VarGenerator varGen,
                                 RacContext ctx,
                                 JExpression expr,
                                 String resultVar,
                                 JTypeDeclarationType typeDecl)
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.
ctx - context to use for the interpretation of undefinedness.
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.
typeDecl - type declaration from which the expression expr comes.

TransExpressionSideEffect

public TransExpressionSideEffect(VarGenerator varGen,
                                 JExpression expr,
                                 String resultVar,
                                 JTypeDeclarationType typeDecl)
Constructs an instance and translates the given expression. If the expression (or its subexpression) encounters an undefinedness, no contextual interpretation is done; i.e., the exception propagates to the caller.

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.
typeDecl - type declaration from which the expression expr comes.
Method Detail

visitAssignmentExpression

public void visitAssignmentExpression(JAssignmentExpression self)
Translates the given assignment expression, self. The translation rule for this expression is defined as follows.
   [[l = E, r]] = 
     T_E v = d_T_E;
     [[E, v]]
     l = v;
 
If l is a reference to a model variable, then it is an error. If l is a reference to a ghost variable, then the setter method must be used instead of the assignment (=).

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

visitCompoundAssignmentExpression

public void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
Translates the given compund assignment expression.

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

visitPrefixExpression

public void visitPrefixExpression(JPrefixExpression self)
Translates the given prefix expression. The translation rule for this expression is defined as follows.
   [[++E, r]] = 
     T_E v = d_T_E;
     [[E, v]]
     v = v + 1;
     E <- v;
     r = v;
 
The expression E should be an l-value. If E is a reference to a ghost variable, its accessor must be used to get and set its value.

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

operator

private static String operator(int opr)
Returns the string representation of the desugared increment or decrement operator.


visitPostfixExpression

public void visitPostfixExpression(JPostfixExpression self)
Translates the given prefix expression. The translation rule for this expression is defined as follows.
   [[E++, r]] = 
     T_E v = d_T_E;
     [[E, v]]
     r = v;
     v = v + 1;
     E <- v;
 
The expression E should denote an l-value. If E is a reference to a ghost variable, its accessor must be used to get and set its value.

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

transAssignmentExpression

public void transAssignmentExpression(JAssignmentExpression expr)
Translates the given assignment expresson.


assignStmt

private RacNode assignStmt(JExpression expr,
                           String var)
Generates a statement that assigns the value of var to expr.


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.