org.jmlspecs.jml4.rac
Class ConstructorBodyTranslator

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

All Implemented Interfaces:

RacConstants

public class ConstructorBodyTranslator
extends MethodBodyTranslator

Translates JML in-line assertions or statements contained in a constructor to RAC code. The translated RAC code is to be parsed and merged into the AST of the constructor body later during the AST merging phase.

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

ConstructorBodyTranslator(CompilationUnitDeclaration source, VariableGenerator varGen)
Creates a new translator for translating constructor bodies of classes contained in the given compilation unit.

Method Summary

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

translateInlineAssertions, translateInlineAssertions

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

ConstructorBodyTranslator

public ConstructorBodyTranslator(CompilationUnitDeclaration source,
                                 VariableGenerator varGen)

Creates a new translator for translating constructor bodies of classes contained in the given compilation unit.