JML

org.jmlspecs.jmlrac
Class TransExpression

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
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor, RacConstants, RacVisitor
Direct Known Subclasses:
TransExpressionSideEffect, TransOldExpression, TransPredicate

public class TransExpression
extends AbstractExpressionTranslator

A RAC visitor class to translate JML expressions into Java source code. The generated code is a sequence of Java statements that evaluate the given expression and store the result into the given variable. The result variable is assumed to be declared in the outer scope that incorporates the code. Both the expression to be translated and the result variable is passed into as arguments of the constructors of this class.

Exceptions and Undefinedness A Java expression can throw an exception. In both mathematical and computational models, we must handle the undefinedness caused by exception. Ideally, we would like to deal with exceptions by having the evaluation of predicates substitute an arbitrary expressible value of the normal result type when an exception is thrown during evaluation [JML]. In practice, however, the runtime asserton checker must determine the definite value for top-level predicates to determine the truth of assertions, e.g., pre- and postcondition violations. There are at least threee possibilities to cope with this problem.

In this implementation, we take the third approach --- the context-sensitive non-strict interpretation. The idea is to ignore an exception as long as it does not affect the evaluation of the top-level predicate, and, if it does, to let the exception contribute to the evaluation toward making the predicate false, but not true.

Nonexecutable Expressions A nonexecutable expression poses a similar problem, and we take a similar approach. But in this case, we take an angelic view. That is, a nonexecutable subexpression is not interpreted if its result does not contribute the truth of the top-level predicate. But if it does, it is interpreted in such a way to making the truth of the top-level predicate true. For example, a precondition of the form "requires (* any informal description *);" is interpreted as being satisfied.

Version:
$Revision: 1.104 $
Author:
Yoonsik Cheon

Nested Class Summary
static class TransExpression.DiagTerm
          A class representing a term to be presented when an assertion is violated.
private static class TransExpression.DynamicCallArg
          A private data structure class for stroring information about arguments for dynamic calls.
private static class TransExpression.StringAndNodePair
          A private data structure class for stroring a pair of String and RacNode objects.
 
Field Summary
protected  RacContext context
          Current translation context.
private  Set diagTerms
          The set of diagnostic terms.
private static Object DT_RESULT
          Special object to denote "\result" in the set of diagnostic terms.
private static Object DT_THIS
          Special object to denote "this" in the set of diagnostic terms.
protected  JExpression expression
          Expression to translate.
protected  Stack paramStack
          Stack for passing parameters to visitor methods.
protected  Stack resultStack
          Stack for returning result from visitor methods.
protected  String resultVar
          Variable to hold the reslt of the target expression.
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
TransExpression(VarGenerator varGen, RacContext ctx, JExpression expr, String resultVar, JTypeDeclarationType typeDecl)
          Constructs an instance and translates the given expression.
 
Method Summary
protected  void addDiagTerm(Object term)
          Adds the given term to the set of terms to be printed when the assertion is violated.
protected  void addDiagTermResult()
          Adds "\result" to the set of terms to be printed when the assertion is violated.
protected  void addDiagTermThis()
          Adds "this" to the set of terms to be printed when the assertion is violated.
 String applyArrayAccessExpression(String strVar, CType typeAccessor, CType typeNumber)
           
 String applyCast(String v, CType typeDest, CType typeVar)
          Returns a string that represents the Java code that casts v of type typeVar to typeDest.
static String applyOperator(String v1, String v2, String binOp, CType type)
          Returns a string that represents the Java code that applies the given operator, binOp, to the given operands, v1 and v2.
static String applyOperator(String v, String unaryOp, CType type)
          Returns a string that represents the Java code that applies the given operator, unaryOp, to the given operand v1.
private  TransExpression.DynamicCallArg argumentsForDynamicCall(JExpression[] args, CSpecializedType[] ptypes)
          Returns an object that contains information about translating arugments, args to a method call for making a dynamic call.
private  TransExpression.StringAndNodePair argumentsForStaticCall(JExpression[] args, String demvar, String angvar)
          Returns a pair of String and RacNode that is the translation of the given argument, args.
protected  void booleanNonExecutableExpression()
          Translates a non-executable boolean expression.
static boolean canMakeStaticCall(JClassFieldExpression expr, String receiver)
          Returns true if a static (non-dynamic) call can be made to the given field expression, expr.
private  RacNode checkUndefined(String demvar, String angvar)
           
static String defaultValue(CType type)
          Returns the default value of the type type.
protected  String diagTerms(String var)
          Returns a string representation of Java statements that, if executed, prints the values of diagnostic terms accumulated so far and stores them to the given variable, var.
protected  String freshVar()
          Returns a fresh variable name.
protected  String GET_ARGUMENT()
          Returns the top element of the parameter stack.
 Object GET_RESULT()
          Returns the top element of the result stack.
protected  RacNode guardUndefined(RacContext ctx, RacNode stmt, String var)
          Returns a new RacNode that wraps the given statement, stmt, inside a try-catch statement to guard against undefinedness caused by runtime exceptions and non-executable expression.
private  RacNode guardUndefined(RacContext ctx, RacNode stmt, CType restype, String resvar, String demvar, String angvar)
           
protected  boolean hasDiagTerms()
          Returns true if there is any diagnostic terms accumulated.
protected  void initDiagTerms()
          Initializes the set of terms to be printed when the assertion is violated.
protected  boolean isNonExecutableFieldReference(JClassFieldExpression expr)
          Returns true if the referenced field (by the argument expression) is not executable.
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.
private  void needDynamicInvocationMethod()
          Records that we need to generate the dynamic invocation method.
protected  void nonExecutableExpression()
          Translates a non-executable non-boolean expression.
private  String optLHS(JMethodCallExpression expr, String var)
          Returns the optional left-hand-side of assignment statement to store the result of evaluation method call expression.
protected  String PEEK_ARGUMENT()
          Peeks the top element of the parameter stack.
protected  void perform()
          Translates the current expression into a sequence of Java statements that evaluate and store the result in the result variable.
 void PUT_ARGUMENT(Object obj)
          Puts the given object to the parameter stack.
private  RacNode receiverForDynamicCall(JExpression expr)
          Returns the receiver for executing the given expression, expr using a dynamic call.
protected  void RETURN_RESULT(Object obj)
          Puts the given object to the result stack.
static boolean specAccessorNeeded(long modifiers)
          Returns true if the modifiers indicate that we need to generate specification-only accessor method.
 RacNode stmt()
          Returns the result of translating the expression.
protected  String toString(CType type)
          Returns the string representation of the given type.
private  RacNode transFieldReference(JClassFieldExpression self, String resultVar, String accPrefix)
          Translates a class field expression that references a model, ghost, spec_public, or spec_protected field.
protected  RacNode translate(JPhylum node, String var)
          Translates an AST into Java statements.
protected  RacNode translate(JPhylum node, String resvar, String demvar, String angvar)
          Translates an AST into Java statements.
 void translateEquivalence(JmlRelationalExpression self)
          Translates the given equivalence expression.
 void translateImplication(JmlRelationalExpression self)
          Translates the given logical implication expression.
 void translateIsSubtypeOf(JmlRelationalExpression self)
          Translates the given isSubtypeOf expression.
private  void translateNonExecutableFieldExpression(JClassFieldExpression expr)
          Translates the given field expression that is determined to be non-executable.
private  RacNode translatePrimitiveType(CType type, String var)
          Translates the given primitive type.
private  void translateToDynamicCall(JMethodCallExpression expr, boolean isModel)
          Translates the given method call expression, expr, into a dynamic call expression.
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 translateToNonexecutableCall(JMethodCallExpression expr)
          Translates the given (model) method call into a non-executable method call.
private  void translateToStaticCall(JMethodCallExpression self, long kind)
          Translates the given method call expression into a static call.
private  void translateToStaticNewObjectExpression(JNewObjectExpression self, boolean isSpecPublic)
          Translates the given new object expression into a static call.
private  String transLocalVariable(JLocalVariableExpression self)
           
protected  RacNode transPrefix(JExpression prefix, String format)
          Translates a prefix of a field or method call expression, build a RacNode using the given format, and return the result.
protected  RacNode transPrefixSpec(JExpression prefix, String format, boolean addDelegee)
           
 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 a binary expression of the given operator.
 void visitBitwiseExpression(JBitwiseExpression self)
          Translates a Java bitwise AND, OR or XOR expression (|, & and ^).
protected  void visitBooleanBinaryExpression(JBinaryExpression self, String oper)
          Translates a binary expression of the given operator.
 void visitBooleanLiteral(JBooleanLiteral self)
          Translates a boolean literal.
protected  void visitByteLiteral(byte value)
          Translates a byte literal.
 void visitCastExpression(JCastExpression self)
          Translates a Java 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 Java logical AND expression (&&).
 void visitConditionalExpression(JConditionalExpression self)
          Translates a Java conditional expression.
 void visitConditionalOrExpression(JConditionalOrExpression self)
          Translates a Java logical OR expression (||).
 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.
 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)
          Translates the given JML \elemtype expression.
 void visitJmlFreshExpression(JmlFreshExpression self)
          Translates a JML \fresh expression.
 void visitJmlInformalExpression(JmlInformalExpression self)
          Translates a JML informal description expression.
 void visitJmlInvariantForExpression(JmlInvariantForExpression self)
          Translates a JML invariant_for expression.
 void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
          Translates a JML \is_initialized expression.
 void visitJmlLabelExpression(JmlLabelExpression self)
          Translates a JML label expression.
 void visitJmlLockSetExpression(JmlLockSetExpression self)
          Translates a JML \lockset expression.
 void visitJmlMaxExpression(JmlMaxExpression self)
           
 void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
          Translates a JML \nonnullelements expression.
 void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
          Translates a JML \not_assigned expression.
 void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
          Translates a JML \not_modified expression.
 void visitJmlOldExpression(JmlOldExpression self)
          Translates a JML \old expression.
 void visitJmlPredicate(JmlPredicate self)
          Translates the given JML predicate.
 void visitJmlPreExpression(JmlPreExpression self)
          Translates a JML \pre expression.
 void visitJmlReachExpression(JmlReachExpression self)
          Translates a JML \reach expression.
 void visitJmlRelationalExpression(JmlRelationalExpression self)
          Translates a JML relational expression.
 void visitJmlResultExpression(JmlResultExpression self)
          Translates a JML \result expression.
 void visitJmlSetComprehension(JmlSetComprehension self)
          Translates a JML set comprehension expression.
 void visitJmlSpecExpression(JmlSpecExpression self)
          Translates a JML specification expression.
 void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
          Translates a JML quantified expression.
 void visitJmlTypeExpression(JmlTypeExpression self)
          Translates a JML \type expression.
 void visitJmlTypeOfExpression(JmlTypeOfExpression self)
          Translates a JML \typeof expression.
 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 object allocator expression.
 void visitNullLiteral(JNullLiteral self)
          Translates a null literal.
 void visitOrdinalLiteral(JOrdinalLiteral self)
          Translates an ordinal literal.
 void visitParenthesedExpression(JParenthesedExpression self)
          Translates a Java parenthesized expression.
 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, a refinement of JML predicate.
 void visitRealLiteral(JRealLiteral self)
          Translates a real literal.
 void visitRelationalExpression(JRelationalExpression self)
          Translates a Java relational expression (<, <=, >, or >=).
 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)
          Translates a Java super expression.
 void visitThisExpression(JThisExpression self)
          Translates a Java this expression.
 void visitTypeNameExpression(JTypeNameExpression self)
          Translates a Java type name expression
 void visitUnaryExpression(JUnaryExpression self)
          Translates a Java unary expression.
 void visitUnaryPromoteExpression(JUnaryPromote self)
          Translates a Java unary promotion expression.
static void warn(TokenReference tref, MessageDescription description, Object obj)
          Produce a warning message with the given token reference, message description, and argument to message description.
protected  RacNode wrapBooleanResult(RacNode argEval, String stmt, String resVar, String demVar, String angVar)
           
protected  RacNode wrapBooleanResultTC(RacNode argEval, String stmt, String resVar, String demVar, String angVar)
           
 RacNode wrappedStmt(String eval, String nval)
          Returns the result of translating the expression wrapped in a try-catch statement to assign the given default values if an exception or non-executability happens while evaluating the expression.
 
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

diagTerms

private Set diagTerms
The set of diagnostic terms. I.e., terms to be printed when the assertion gets violated.

 private invariant (\forall Object o; diagTerms.contains(o); 
   (o instanceof JFormalParameter) || (o instanceof String) ||
   (o instanceof JmlVariableDefinition) ||
   o == DT_THIS || o == DT_RESULT);
 


DT_THIS

private static final Object DT_THIS
Special object to denote "this" in the set of diagnostic terms.


DT_RESULT

private static final Object DT_RESULT
Special object to denote "\result" in the set of diagnostic terms.


varGen

protected VarGenerator varGen
Generator of unique variable names.


resultVar

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


paramStack

protected Stack paramStack
Stack for passing parameters to visitor methods.


resultStack

protected Stack resultStack
Stack for returning result from visitor methods.


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?

Constructor Detail

TransExpression

public TransExpression(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.
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()
Returns the result of translating the expression. The returned code is not wrapped in a try-catch statement that caches exceptions and non-executable specifications in the expression.

 normal_behavior
   assignable translated;
   ensures \fresh(\result) && \result != null && 
     (* \result is the translation result *);
 

Returns:
translation result
See Also:
#wrappedStmt()

wrappedStmt

public RacNode wrappedStmt(String eval,
                           String nval)
Returns the result of translating the expression wrapped in a try-catch statement to assign the given default values if an exception or non-executability happens while evaluating the expression. The returned code has the following structure.
 try {
  [[E, r]]
 } catch (JMLNonExecutableException e) {
  r = nval;
 } catch (Exception e) {
  r = eval;
 }
 
where E is the target expression to translate and r is the variable to hold the result of the expression.

 normal_behavior
   assignable translated;
   ensures \fresh(\result) && \result != null && 
     (* \result is a try-catch statement wrapping translation result *);
 

Parameters:
eval - default value for exceptions. If the given expression (or one of its subexpressions) throws an exception during evaluation, the value given by this parameter is used as the result.
nval - default value for non-executable expressions.
Returns:
translation result wrapped in a try-catach block
See Also:
stmt()

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.

   requires !translated;
   assignable translated;
   ensures translated && (* translation is performed *);
 also
   requires translated;
   ensures (* no translation is performed *);
 


visitRacPredicate

public void visitRacPredicate(RacPredicate self)
Translates the given RAC predicate, a refinement of JML predicate. The translation rule for this expression is defined as follows.
   [[P, r]] =
     [[expr(P), r]]
     if (!r) {
        VN_ERROR_SET.add(loc(P));
     }
 
where expr(P) denotes the unwrapped JML specification expression of P, VN_ERROR_SET is a variable name for keeping track of violated assertions and loc(P) denotes the location that the predicate P appears in the source file.

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

visitJmlPredicate

public void visitJmlPredicate(JmlPredicate self)
Translates the given JML predicate. The translation rule for this expression is defined as follows.
   [[P, r]] = [[expr(P), r]]
 
where expr(P) denotes the unwrapped JML specification expression of P.

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

visitJmlSpecExpression

public void visitJmlSpecExpression(JmlSpecExpression self)
Translates a JML specification expression. The translation rule for this expression is defined as follows.
   [[E, r]] = [[expr(E), r]]
 
where expr(E) denotes the unwrapped Java expression of E.

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

visitJmlNonNullElementsExpression

public void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
Translates a JML \nonnullelements expression. The translation rule for this expression is defined as follows.
   [[\nonnullelements(E), r]] =
     T_E v = d_T_E;
     [[E, v]]
     r = v != null;
     if (r) {
        for (int i = 0; r && i < v.length; i++) {
            r = v[i] != null;
        }
     }
 
where T_E is the type of expression E and d_T_E is the default value of the type T_E.

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

visitJmlElemTypeExpression

public void visitJmlElemTypeExpression(JmlElemTypeExpression self)
Translates the given JML \elemtype expression. The translation rule for this expression is defined as follows (thanks to Erik Poll) - adjusted DRC.
   [[\elemtype(E)), r]] = 
     r = [[E]].getComponentType();
 

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

visitJmlNotModifiedExpression

public void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
Translates a JML \not_modified expression. The translation rules for this expression is defined as follows.
   [[\not_modified(E)), r]] = \not_executable
 

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

visitJmlNotAssignedExpression

public void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
Translates a JML \not_assigned expression. The translation rules for this expression is defined as follows.
   [[\not_assigned(E)), r]] = \not_executable
 

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

visitJmlFreshExpression

public void visitJmlFreshExpression(JmlFreshExpression self)
Translates a JML \fresh expression. The translation rules for this expression is defined as follows.
   [[\fresh(E)), r]] = \not_executable
 

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

visitJmlInformalExpression

public void visitJmlInformalExpression(JmlInformalExpression self)
Translates a JML informal description expression. The translation rules for this expression is defined as follows.
   [[(* ... *), r]] = \not_executable
 

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

visitJmlInvariantForExpression

public void visitJmlInvariantForExpression(JmlInvariantForExpression self)
Translates a JML invariant_for expression. The translation rules for this expression is defined as follows.
   [[\invariant_for(E), r]] = 
     T_E v = d_T_E;
     [[E, v]]
     r = v.inv();
 
where inv() is the invariant method of type T_E. A special treatment is required if v is null.

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

visitJmlIsInitializedExpression

public void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
Translates a JML \is_initialized expression. The translation rules for this expression is defined as follows.
   [[\is_initialized(T), r]] = 
     try {
       r = T.class.getDeclaredField(VN_RAC_COMPILED).getBoolean(null);
     } catch (Exception e) {
       r = true;
     }
 

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

visitJmlLabelExpression

public void visitJmlLabelExpression(JmlLabelExpression self)
Translates a JML label expression. The translation rules for this expression is defined as follows.
   [[(\lblneg n E), r]] = [[E, r]]
   [[(\lblpos n E), r]] = [[E, r]]
 
Though not shown in the translation rule, the label of the given expression is added to VN_ERROR_SET if the expression does not (or does) hold depending on the kind of label.

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

visitJmlLockSetExpression

public void visitJmlLockSetExpression(JmlLockSetExpression self)
Translates a JML \lockset expression. The translation rules for this expression is defined as follows.
   [[\lockset, r]] = \not_executable
 

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

visitJmlOldExpression

public void visitJmlOldExpression(JmlOldExpression self)
Translates a JML \old expression. The translation rules for this expression is defined as follows.
   [[\old(E), r]] = 
      r = v;  
 
with an insertion of T_E v = d_T_E; [[E, v]] into the method prolog.

Specified by:
visitJmlOldExpression in interface JmlVisitor
Overrides:
visitJmlOldExpression in class JmlAbstractVisitor
See Also:
TransPostcondition, TransOldExpression

visitJmlPreExpression

public void visitJmlPreExpression(JmlPreExpression self)
Translates a JML \pre expression. The translation rules for this expression is defined as follows.
   [[\pre(E), r]] = 
      r = v;  
 
with an insertion of T_E v = d_T_E; [[E, v]] into the method prolog.

Specified by:
visitJmlPreExpression in interface JmlVisitor
Overrides:
visitJmlPreExpression in class JmlAbstractVisitor
See Also:
TransPostcondition, TransOldExpression

visitJmlReachExpression

public void visitJmlReachExpression(JmlReachExpression self)
Translates a JML \reach expression. The translation rules for this expression is defined as follows.
   [[\reach(E), r]] = \not_executable 
 

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

visitJmlResultExpression

public void visitJmlResultExpression(JmlResultExpression self)
Translates a JML \result expression. The translation rules for this expression is defined as follows.
   [[\result, r]] = 
     r = result;
 
where the variable result is used to capture the return value of the method. The statement T result = d_T; gets inserted into the method prolog, where T is the return type of the method.

Specified by:
visitJmlResultExpression in interface JmlVisitor
Overrides:
visitJmlResultExpression in class JmlAbstractVisitor
See Also:
TransPostcondition

visitJmlSetComprehension

public void visitJmlSetComprehension(JmlSetComprehension self)
Translates a JML set comprehension expression. The translation rule for this expression is defined as follows.
   [[new S { T x | E.has(x) && P}, r]] = 
     T_E c = null;
     [[E, c]]
     r = new S();
     Iterator iter = c.iterator();
     for (iter.hasNext()) {
         T x = iter.next();
         boolean b = false;
         [[P, b]]
         if (b) {
            r.add(x);
         }
     }
 

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

visitJmlSpecQuantifiedExpression

public void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
Translates a JML quantified expression. The translation rules for the JML universal/existential quantified expressions are defined as follows. The rules for other quantifiers are defined in a similar way.
   [[(\forall T x; P; Q), r]] =
     Collection c = null;
     [[S, c]]  // S is the qset of P ==> Q
     r = c != null;
     if (r) {
        Iterator iter = c.iterator();
        for (r && iter.hasNext()) {
            T x = iter.next();
            [[P ==> Q, r]]
        }
     }
 
   [[(\exists T x; P; Q), r]] =
     Collection c = null;
     [[S, c]]  // S is the qset of P && Q
     r = c == null;
     if (!r) {
        Iterator iter = c.iterator();
        for (!r && iter.hasNext()) {
            T x = iter.next();
            [[P && Q, r]]
        }
     }
 

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

visitJmlTypeExpression

public void visitJmlTypeExpression(JmlTypeExpression self)
Translates a JML \type expression. If the expression is of primitive types, the result is the Java predefined Class object representing the primitive type, e.g., Integer.TYPE for int. Otherwise, the following translation rule is applied.
   [[\type(E), r]] = 
     r = E.class;
 

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

translatePrimitiveType

private RacNode translatePrimitiveType(CType type,
                                       String var)
Translates the given primitive type. E.g., for the type int, the result is "var = Integer.TYPE;".

 requires type != null && type.isPrimitive() && var != null;
 ensures \result != null;
 


visitJmlTypeOfExpression

public void visitJmlTypeOfExpression(JmlTypeOfExpression self)
Translates a JML \typeof expression. If the expression is of primitive types, the result is the Java predefined Class object representing the primitive type, e.g., Integer.TYPE for int. Otherwise, the following translation rule is applied.
   [[\typeof(E), r]] = 
    T v;
    [[E, v]]
    if (v == null)
      r = java.lang.Object; // !FIXME!\typeof(null)
    else
      r = v.getClass();
 

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

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.


visitConditionalExpression

public void visitConditionalExpression(JConditionalExpression self)
Translates a Java conditional expression. The translation rule for the conditional expression is defined as follow.
   [[E1 ? E2 : E3, r]] =
     boolean v = false;
     [[E1, v]]
     if (v1) {
        [[E2, r]]
     }
     else {
        [[E3, r]]
     }
 

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

visitJmlRelationalExpression

public void visitJmlRelationalExpression(JmlRelationalExpression self)
Translates a JML relational expression. If the expression is a subtype-of expression, the following translation rule is used. expression.
   [[E1 <: E2, r]] =
     Class v1 = null;
     Class v2 = null;
     [[E1, v1]]
     [[E2, v2]]
     r = v2.isisAssignableFrom(v1);
 
Otherwise (i.e., for <==>, <=!=>, ==>, and <==, the following translation rule is used.
   [[E1 op E2, r]] =
     boolean v1 = false;
     boolean v2 = false;
     [[E1, v1]]
     [[E2, v2]]
     r = [[v1,v2,op]];
 
where the translation [[v1,v2,op]] is defined as follow.
   v1 <==> v2 = v1 == v2
   v1 <=!=> v2 = v1 != v2
   v1 ==> v2 = v1 ? v2 : true
   v1 <== v2 = v2 ? v1 : true
 
Note: there is also the case of comparing locks with < or <=

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

translateIsSubtypeOf

public void translateIsSubtypeOf(JmlRelationalExpression self)
Translates the given isSubtypeOf expression.

 requires self.isSubtypeOf();
 


wrapBooleanResult

protected RacNode wrapBooleanResult(RacNode argEval,
                                    String stmt,
                                    String resVar,
                                    String demVar,
                                    String angVar)

wrapBooleanResultTC

protected RacNode wrapBooleanResultTC(RacNode argEval,
                                      String stmt,
                                      String resVar,
                                      String demVar,
                                      String angVar)

translateImplication

public void translateImplication(JmlRelationalExpression self)
Translates the given logical implication expression.

 requires self.isImplication() || self.isBackwardImplication();
 


translateEquivalence

public void translateEquivalence(JmlRelationalExpression self)
Translates the given equivalence expression.

 requires self.isEquivalence() || self.isNonEquivalence();
 


visitConditionalAndExpression

public void visitConditionalAndExpression(JConditionalAndExpression self)
Translates a Java logical AND expression (&&). The translation rule for the logical AND expression is defined as follow.
   [[E1 && E2, r]] =
     [[E1, r]]
     if (r) {
        [[E2, r]]
     }
 

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

checkUndefined

private RacNode checkUndefined(String demvar,
                               String angvar)

visitConditionalOrExpression

public void visitConditionalOrExpression(JConditionalOrExpression self)
Translates a Java logical OR expression (||). The translation rule for the logical OR expression is defined as follow.
   [[E1 || E2, r]] =
     [[E1, r]]
     if (!r) {
        [[E2, r]]
     }
 

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

visitBitwiseExpression

public void visitBitwiseExpression(JBitwiseExpression self)
Translates a Java bitwise AND, OR or XOR expression (|, & and ^). The translation rule for the bitwise expression is defined as follow.
   [[E1 opr E2, r]] =
     T_E1 v1 = d_T_E1;
     T_E2 v2 = d_T_E2;
     [[E1, v1]]
     [[E2, v2]]
     r = v1 opr v2;
 

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

visitEqualityExpression

public void visitEqualityExpression(JEqualityExpression self)
Translates an equality expression. The translation rule for the equality expression is defined as follows.
   [[E1 opr E2, r]] =
     T_E1 v1 = d_T_E1;
     T_E2 v2 = d_T_E2;
     [[E1, v1]]
     [[E2, v2]]
     r = v1 opr v2;
 

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

applyOperator

public static String applyOperator(String v1,
                                   String v2,
                                   String binOp,
                                   CType type)
Returns a string that represents the Java code that applies the given operator, binOp, to the given operands, v1 and v2. This method handles both relational and arithmetic operators. When type is not Bigint this is simple: e.g. with "+", "1" and "2" as values for binOp, v1 and v2 respectively, the return value will be "1 + 2". Special treatment is done to appropriately handle Bigint expressions -- e.g. for addition the equivalent of "v1.add(v2)" is returned.

See Also:
visitBinaryExpression(org.multijava.mjc.JBinaryExpression, java.lang.String)

visitRelationalExpression

public void visitRelationalExpression(JRelationalExpression self)
Translates a Java relational expression (<, <=, >, or >=). The translation rule for the relational expression is defined as follow.
   [[E1 opr E2, r]] =
     try {
       T_E1 v1 = d_T_E1;
       T_E2 v2 = d_T_E2;
       [[E1, v1]]
       [[E2, v2]]
       r = v1 opr v2;
     }
     catch (Exception e) {
       r = false;
     }
 

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

visitInstanceofExpression

public void visitInstanceofExpression(JInstanceofExpression self)
Translates a Java instanceof expression. The translation rule for the instanceof expression is defined as follow.
   [[E1 instanceof T, r]] =
     try {
       T_E1 v = d_T_E1;
       [[E1, v]]
       r = v instanceof T;
     }
     catch (Exception e) {
       r = false;
     }
 

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

visitBinaryExpression

protected void visitBinaryExpression(JBinaryExpression self,
                                     String oper)
Translates a binary expression of the given operator.

Overrides:
visitBinaryExpression in class JmlAbstractVisitor

visitBooleanBinaryExpression

protected void visitBooleanBinaryExpression(JBinaryExpression self,
                                            String oper)
Translates a binary expression of the given operator.


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

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

visitUnaryExpression

public void visitUnaryExpression(JUnaryExpression self)
Translates a Java unary expression. These are (+, -, ~, and !. The translation rules for this expression is defined as follows.
   [[opr E, r]] = 
      [[E, r]]
      r = opr r;
 
We need a special treatment for the operator ! to change the default return value used if there occurrs an exception while evaluating a subexpression.

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

applyOperator

public static String applyOperator(String v,
                                   String unaryOp,
                                   CType type)
Returns a string that represents the Java code that applies the given operator, unaryOp, to the given operand v1.

See Also:
TransExpression#applyOperator(String v1, String v2, String binOp, CType type), visitUnaryExpression(org.multijava.mjc.JUnaryExpression)

visitCastExpression

public void visitCastExpression(JCastExpression self)
Translates a Java cast expression. The translation rules for this expression is defined as follows.
   [[(T) E, r]] = 
      T_E v = d_T_E;
      [[E, v]]
      r = (T) v;
 

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

applyCast

public String applyCast(String v,
                        CType typeDest,
                        CType typeVar)
Returns a string that represents the Java code that casts v of type typeVar to typeDest.

See Also:
visitCastExpression(org.multijava.mjc.JCastExpression)

visitUnaryPromoteExpression

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

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

visitMethodCallExpression

public void visitMethodCallExpression(JMethodCallExpression self)
Translates a Java method call expression. The general translation rule for the java method call expression is defined as follow.
   [[E0.m(E1, ..., En), r]] =
     T_E0 v0 = d_T_E0;
     T_E1 v1 = d_T_E1;
     ...
     T_En vn = d_T_En;
     [[E0, v0]]
     [[E1, v1]]
     ...
     [[En, vn]]
     r = v0.m(v1, ..., vn);
 
If the referenced method, m, is an effectively model method (including the ones declared in model types), there are three possibilities. If the method is not executable (i.e., has no body), then the method call expression is translated into an angelic undefinedness. Otherwise, the expression is translated into either a static or dynamic call to the model method. If the model method is declared in the same class or interface where the assertion being translated in specified, then static call is used; otherwise, dynamic call is used.

A spec_public or spec_protected method call expression is always executable, and is translated into either a dynamic or static call.

Specified by:
visitMethodCallExpression in interface MjcVisitor
Overrides:
visitMethodCallExpression in class JmlAbstractVisitor
See Also:
TransType.dynamicCallNeeded(CClass), translateToDynamicCall(JMethodCallExpression, boolean), translateToNonexecutableCall(JMethodCallExpression), #tranlateToStaticCall(JMethodCallExpression, int), addDiagTermThis(), visitNewObjectExpression(JNewObjectExpression)

translateToNonexecutableCall

private void translateToNonexecutableCall(JMethodCallExpression expr)
Translates the given (model) method call into a non-executable method call.

See Also:
visitMethodCallExpression(JMethodCallExpression)

translateToStaticCall

private void translateToStaticCall(JMethodCallExpression self,
                                   long kind)
Translates the given method call expression into a static call. If the argument, kind, is ACC_MODEL, the given expression is assumed to be a model method call expression that can be translated into a static call (e.g., called in the same type where the method is declared). In such a case, the expression is translated into a call to the appropriate surrogate object if the called model method is declared in an interface. If the argument, kind, is ACC_SPEC_PUBLIC, the given expression is assumed to be a spec_public method call expression, for which we have to call the corresponding access method. Otherwise, it is assumed to be a regular method call expression.

 requires self != null;
 requires kind == ACC_MODEL || kind == ACC_SPEC_PUBLIC ||
          kind == 0; 
 

See Also:
visitMethodCallExpression(JMethodCallExpression)

guardUndefined

private RacNode guardUndefined(RacContext ctx,
                               RacNode stmt,
                               CType restype,
                               String resvar,
                               String demvar,
                               String angvar)

optLHS

private String optLHS(JMethodCallExpression expr,
                      String var)
Returns the optional left-hand-side of assignment statement to store the result of evaluation method call expression. That is, if the type of the method call is void, an empty string is returned; otherwise, a string var + " = " is returned.


argumentsForStaticCall

private TransExpression.StringAndNodePair argumentsForStaticCall(JExpression[] args,
                                                                 String demvar,
                                                                 String angvar)
Returns a pair of String and RacNode that is the translation of the given argument, args. The string of the pair has the form: "(v1, v2, ..., vn)", and the node has the form: T1 v1 = E1; ...; Tn vn = En;, where Ei is the i-th element of the argument args. The variable vi is a fresh new variable. If the argument, args, is null or an empty array, the string of the pair is "()" and the node is null. The result is always non-null.

 ensures \result != null;
 


transPrefix

protected RacNode transPrefix(JExpression prefix,
                              String format)
Translates a prefix of a field or method call expression, build a RacNode using the given format, and return the result. The returned code has the following form:
  T v = T_init;
  [[code for eval prefix and assigning to v]]
  format[v/$0]
 

  requires prefix != null && format != null;
  ensures \result != null;
 

Parameters:
prefix - the prefix to be translated.
format - the format to build the return value out of the translated prefix; it is usually of the form: "r = $0.m(x1, ..., xn);" or "r = $0.f;.
See Also:
visitMethodCallExpression(org.multijava.mjc.JMethodCallExpression), visitFieldExpression(org.multijava.mjc.JClassFieldExpression), #transPrefix(JExpression, String, CClass, isModel)

transPrefixSpec

protected RacNode transPrefixSpec(JExpression prefix,
                                  String format,
                                  boolean addDelegee)

translateToDynamicCall

private void translateToDynamicCall(JMethodCallExpression expr,
                                    boolean isModel)
Translates the given method call expression, expr, into a dynamic call expression. If the argument, isModel, is true, it is treated as a call to a model method, thus; otherwise, it is treated as a call to a spec_public or spec_protected method. This flag is used to determine appropriate access methods.

See Also:
visitMethodCallExpression(JMethodCallExpression)

argumentsForDynamicCall

private TransExpression.DynamicCallArg argumentsForDynamicCall(JExpression[] args,
                                                               CSpecializedType[] ptypes)
Returns an object that contains information about translating arugments, args to a method call for making a dynamic call. The argument, ptypes, is supposed to be the parameter types of the called method. The field node of the returned object has code of the form: T1 v1 = E1; ...; Tn vn = En;, where Ei is the i-th element of the argument args. The field types has the form: " "new Class[] { T1, ..., Tn }", where Ti is the i-th parameter type, and the field args has the form: "new Object[] { v1, ..., vn }"."(v1, v2, ..., vn)". The variable vi is a fresh new variable. If the argument, args, is null or an empty array, the node field becomes null and the other two fields become "new Class[] {}" and "new Object[] {}" respectively. The result is always non-null.

 ensures \result != null;
 

See Also:
translateToDynamicCall(JMethodCallExpression, boolean), translateToDynamicNewObjectExpression(JNewObjectExpression,boolean), #DynamicCallArg

receiverForDynamicCall

private RacNode 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.

 requires expr != null && expr instanceof JMethodCallExpression &&
   expr instanceof JClassFieldExpression;
 


visitTypeNameExpression

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

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

visitThisExpression

public void visitThisExpression(JThisExpression self)
Translates a Java this expression. The translation rule for "this" expression is defined as:
   [[E.this, r]] = 
      r = E.this;
 
In an interface, however, "this" is translated into the private delegee field of the surrogate class.

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

visitSuperExpression

public void visitSuperExpression(JSuperExpression self)
Translates a Java super expression. The translation rules for this expression is defined as follows.
   [[super, r]] = 
      r = super;
 

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

visitClassExpression

public void visitClassExpression(JClassExpression self)
Translates a Java class expression. The translation rules for this expression is defined as follows.
   [[T.class, r]] = 
      r = T.class;
 

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

visitArrayLengthExpression

public void visitArrayLengthExpression(JArrayLengthExpression self)
Translates a Java array length expression. The translation rules for this expression is defined as follows.
   [[E.length, r]] = 
      T_E v = d_T_E;
      [[E, v]]
      r = v.length;
 

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

visitArrayAccessExpression

public void visitArrayAccessExpression(JArrayAccessExpression self)
Translates a Java array access expression. The translation rules for this expression is defined as follows.
   [[E1[E2], r]] = 
      T_E1 v1 = d_T_E1;
      T_E2 v2 = d_T_E2;
      [[E1, v1]]
      [[E2, v2]]
      r = v1[v2];
 

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

applyArrayAccessExpression

public String applyArrayAccessExpression(String strVar,
                                         CType typeAccessor,
                                         CType typeNumber)

visitNameExpression

public void visitNameExpression(JNameExpression self)
Translates a Java name expression. The translation rules for this expression is defined as follows.
   [[n, r]] = 
      r = n;
 

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

visitLocalVariableExpression

public void visitLocalVariableExpression(JLocalVariableExpression self)
Translates a Java local variable expression. The translation rules for this expression is defined as follows.
   [[x, r]] = 
      r = x;
 

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

transLocalVariable

private String transLocalVariable(JLocalVariableExpression self)

visitParenthesedExpression

public void visitParenthesedExpression(JParenthesedExpression self)
Translates a Java parenthesized expression. The translation rules for this expression is defined as follows.
   [[(E), r]] = [[E, r]]
 

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

visitNewObjectExpression

public void visitNewObjectExpression(JNewObjectExpression self)
Translates a Java object allocator expression. The general translation rule for the Java object allocator expression is defined as follow.
   [[new T(E1, ..., En), r]] =
     T_E1 v1 = d_T_E1;
     ...
     T_En vn = d_T_En;
     [[E1, v1]]
     ...
     [[En, vn]]
     r = new T(v1, ..., vn);
 
If the referenced constructor is effectively model (including constructors declared in model types), there are three possibilities. If the constructor is not executable (i.e., has no body), then the expression is translated into an angelic undefinedness. Otherwise, the expression is translated into either a static or dynamic call to the model constructor. If the model constructor comes from the same class or interface where the assertion being translated in specified, then static call is used; otherwise, dynamic call is used.

A spec_public or spec_protected constructor is always executable, and is translated into either a dynamic or static call.

Specified by:
visitNewObjectExpression in interface MjcVisitor
Overrides:
visitNewObjectExpression in class JmlAbstractVisitor
See Also:
TransType.dynamicCallNeeded(CClass), nonExecutableExpression(), translateToStaticNewObjectExpression(JNewObjectExpression,boolean), translateToDynamicNewObjectExpression(JNewObjectExpression,boolean), visitMethodCallExpression(JMethodCallExpression)

translateToStaticNewObjectExpression

private void translateToStaticNewObjectExpression(JNewObjectExpression self,
                                                  boolean isSpecPublic)
Translates the given new object expression into a static call. If the argument, isSpecPublic, is false, the translated code has the form:
  T1 v1 = E1; ...; Tn vn = En; 
  result = new T(v1, ..., vn); 
  
Otherwise, the translated code has the following form:
  T1 v1 = E1; ...; Tn vn = En; 
  result = MN_SPEC_PUBLIC$T(v1, ..., vn); 
  


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

visitFieldExpression

public void visitFieldExpression(JClassFieldExpression self)
Translates a Java field expression. The translation rules for this expression is defined as follows.
   [[E.x, r]] = 
     T_E v = d_T_E;
     [[E, v]]
     r = v;
 
If the referenced field is a model field, generates a model method call instead.

Specified by:
visitFieldExpression in interface MjcVisitor
Overrides:
visitFieldExpression in class JmlAbstractVisitor
See Also:
transPrefix(org.multijava.mjc.JExpression, java.lang.String)

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.


translateNonExecutableFieldExpression

private void translateNonExecutableFieldExpression(JClassFieldExpression expr)
Translates the given field expression that is determined to be non-executable.


transFieldReference

private RacNode transFieldReference(JClassFieldExpression self,
                                    String resultVar,
                                    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. The translation rules is defined as follows.
 [[e.x, r]] ==
  T_e v = init_T_e;
  [[e, v]]
  Object o = rac$invoke(C, v, x$C, null, null);
  if (o == null) {
     throw new JMLNonExecutableException();
  }
  r = (T)o;
 
where C is the name of class where x is declared and T is the type of x.

 requires self != null && resultVar != null;
 


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.


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

nonExecutableExpression

protected void nonExecutableExpression()
Translates a non-executable non-boolean expression. The expression is translated into the Java statement of the form: throw new JMLNonExectutableException();. The result variable is popped from the parameter stack and the generated RacNode object is pushed ont the result stack.


booleanNonExecutableExpression

protected void booleanNonExecutableExpression()
Translates a non-executable boolean expression. The expression is translated into either true or false depending on the current polarity of translation. The result variable is popped from the parameter stack and the generated RacNode object is pushed ont the result stack.


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.


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)));
 


translate

protected RacNode translate(JPhylum node,
                            String var)
Translates an AST into Java statements.


translate

protected RacNode translate(JPhylum node,
                            String resvar,
                            String demvar,
                            String angvar)
Translates an AST into Java statements.


guardUndefined

protected RacNode guardUndefined(RacContext ctx,
                                 RacNode stmt,
                                 String var)
Returns a new RacNode that wraps the given statement, stmt, inside a try-catch statement to guard against undefinedness caused by runtime exceptions and non-executable expression. The statement is supposed to store some value to the variable named var.


defaultValue

public static String defaultValue(CType type)
Returns the default value of the type type.


toString

protected String toString(CType type)
Returns the string representation of the given type. If the type is JmlStdType.TYPE, the result is "java.lang.Class"; otherwise it is value.toString().

See Also:
TransUtils.toString(CType)

freshVar

protected String freshVar()
Returns a fresh variable name.


GET_ARGUMENT

protected String GET_ARGUMENT()
Returns the top element of the parameter stack.


PEEK_ARGUMENT

protected String PEEK_ARGUMENT()
Peeks the top element of the parameter stack.


PUT_ARGUMENT

public void PUT_ARGUMENT(Object obj)
Puts the given object to the parameter stack.


GET_RESULT

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


RETURN_RESULT

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


warn

public static void warn(TokenReference tref,
                        MessageDescription description,
                        Object obj)
Produce a warning message with the given token reference, message description, and argument to message description.


initDiagTerms

protected void initDiagTerms()
Initializes the set of terms to be printed when the assertion is violated. This set is called diagnostic terms.


addDiagTerm

protected void addDiagTerm(Object term)
Adds the given term to the set of terms to be printed when the assertion is violated.


addDiagTermThis

protected void addDiagTermThis()
Adds "this" to the set of terms to be printed when the assertion is violated.


addDiagTermResult

protected void addDiagTermResult()
Adds "\result" to the set of terms to be printed when the assertion is violated.


hasDiagTerms

protected boolean hasDiagTerms()
Returns true if there is any diagnostic terms accumulated.


diagTerms

protected String diagTerms(String var)
Returns a string representation of Java statements that, if executed, prints the values of diagnostic terms accumulated so far and stores them to the given variable, var. The returned statements also declares the variable var. If there is no diagnostic terms accumulated so far, then an empty string is returned.


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.