org.jmlspecs.jml4.rac
Class MethodBodyTranslator

java.lang.Object
  org.jmlspecs.jml4.rac.RacTranslator
      org.jmlspecs.jml4.rac.MethodBodyTranslator

All Implemented Interfaces:

RacConstants

Direct Known Subclasses:

ConstructorBodyTranslator

public class MethodBodyTranslator
extends RacTranslator

Translates a method body of a class or interface to RAC code. For classes, this class translates JML in-line assertions and statements contained in a method body to RAC code. For interfaces, it generates bodies for the so-called delegation methods.

Author:

Amritam Sarcar and Yoonsik Cheon

Nested Class Summary

Nested classes/interfaces inherited from interface org.jmlspecs.jml4.rac.RacConstants

RacConstants.Behavior, RacConstants.Condition

Field Summary

Fields inherited from interface org.jmlspecs.jml4.rac.RacConstants

ANNOTATION, AT_GHOST, AT_MODEL, EMPTY_STRING, ENTIRE_CLAUSE, ERROR_NEVER_CALL, ERROR_NOT_IMPL, ERROR_RAC_IMPL, GHOST_METHOD_PREFIX, HELPER, ID_INSTANCE_DOLLAR, ID_STATIC, INTERNAL_CONSTRUCTOR_PREFIX, INTERNAL_METHOD_PREFIX, JML_CHECKABLE, 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, MODEL_METHOD_PREFIX, NON_EXEC, PKG_RAC_RUNTIME, RAC_TMP_FILE_EXTENSION, RAC_TMP_FILE_PREFIX, TN_BOOLEAN, TN_CONSTRAINT_ERROR, TN_ENTRY_PRECONDITON_ERROR, TN_EXIT_EXCEPTIONAL_POSTCONDITION_ERROR, TN_EXIT_NORMAL_POSTCONDITION_ERROR, TN_INVARIANT_ERROR, TN_JMLCACHE, TN_JMLCHECKABLE, TN_JMLSURROGATE, TN_JMLUNIT_TEST_POSTFIX, TN_JMLUNIT_TESTDATA_POSTFIX, TN_JMLVALUE, TN_LOCATION, TN_SURROGATE, TN_VOID, VN_ASSERTION, VN_CATCH_VAR, VN_CLASS_INIT, VN_CONSTRUCTED, VN_DELEGEE, VN_ERROR_SET, VN_EXCEPTION, VN_FREE_VAR, VN_INIT, VN_MSG, VN_NAME, VN_OLD_VAR, VN_PARAMS, VN_POST_VAR, VN_PRE_VAR, VN_PRECOND, VN_RAC_COMPILED, VN_RAC_LEVEL, VN_RESULT, VN_STACK_VAR, VN_VALUE_SET, VN_XRESULT

Constructor Summary

MethodBodyTranslator(CompilationUnitDeclaration source, VariableGenerator varGen)
Creates a new translator for the given compilation unit.

Method Summary

java.lang.StringBuffer	translateInlineAssertions(AbstractMethodDeclaration sourceMethod, RacResult result) Translates all in-line assertions of sourceMethod to RAC code and attach them to targetMethod.
java.lang.StringBuffer	translateInlineAssertions(Initializer initBlock, RacResult result)

Methods inherited from class org.jmlspecs.jml4.rac.RacTranslator

argumentsToString, argumentsToString, createImportForRacRuntimePackage, escapeString, escapeString, escapeString, getBoxedValue, getCharacterNumber, getClassType, getDeclaringClassName, getDeclaringClassName, getDefaultValue, getErrorLocation, getFullyQualifiedName, getFullyQualifiedName, getLineNumber, getRacErrorLocation, getSpecification, getUnboxedValue, getWrapperType, hasVoidReturnType, hasVoidReturnType, isGhostField, isModelField, makeMethod, makeMethod, makeMethod, parameterDeclarationToString, parameterDeclarationToString, racErrorDeclaration, racErrorDefinition, racMethodForName, racMethodsForGhostOrModel, racMethodsForSurrogate, racRuntimeMethods, throwsClauseToString, throwsClauseToString, typeName, typeName, unescapeString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

MethodBodyTranslator

public MethodBodyTranslator(CompilationUnitDeclaration source,
                            VariableGenerator varGen)

Creates a new translator for the given compilation unit.

Method Detail

translateInlineAssertions

public java.lang.StringBuffer translateInlineAssertions(AbstractMethodDeclaration sourceMethod,
                                                        RacResult result)

Translates all in-line assertions of sourceMethod to RAC code and attach them to targetMethod. The RAC code is added to the racCode field. Other translation information is stored in racResult.

Returns:

TODO

translateInlineAssertions

public java.lang.StringBuffer translateInlineAssertions(Initializer initBlock,
                                                        RacResult result)

See Also:

transIn