org.jmlspecs.jml4.rac
Class ClassDeclarationTranslator

java.lang.Object
  org.jmlspecs.jml4.rac.RacTranslator
      org.jmlspecs.jml4.rac.TypeDeclarationTranslator
          org.jmlspecs.jml4.rac.ClassDeclarationTranslator

All Implemented Interfaces:

RacConstants

public class ClassDeclarationTranslator
extends TypeDeclarationTranslator

Translates JML assertions associated with classes to runtime assertion checking (RAC) code. This class is for translating various JML assertions associated with Java classes and their members to RAC code. The translated RAC code will be hosted in a new class declaration node, which is supposed to be pretty printed and parsed and merged to the AST of the source class.

Author:

Amritam Sacar 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

ClassDeclarationTranslator(CompilationUnitDeclaration sourceUnit, CompilationUnitDeclaration targetUnit)
Creates a new translator to translate the given source unit to the target unit.

Method Summary

TypeDeclaration

translate(TypeDeclaration sourceType, TypeDeclaration targetType) Translates JML assertions of sourceType to RAC code and store the RAC code to targetType.

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

needOwnRacRuntimeSupport

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

ClassDeclarationTranslator

public ClassDeclarationTranslator(CompilationUnitDeclaration sourceUnit,
                                  CompilationUnitDeclaration targetUnit)

Creates a new translator to translate the given source unit to the target unit.

Parameters:

sourceUnit - Compilation unit to be translated

targetUnit - Compilation unit to receive translated code

Method Detail

translate

public TypeDeclaration translate(TypeDeclaration sourceType,
                                 TypeDeclaration targetType)

Translates JML assertions of sourceType to RAC code and store the RAC code to targetType.

Overrides:

translate in class TypeDeclarationTranslator

Parameters:

sourceType - Class to be translated to RAC code

targetType - Class to host translated RAC code

Returns:

targetType