org.jmlspecs.jml4.rac
Class MethodHeaderTranslator

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

All Implemented Interfaces:

RacConstants

Direct Known Subclasses:

ConstructorHeaderTranslator

public abstract class MethodHeaderTranslator
extends RacTranslator

Translates a method or constructor header along with its specification such as pre and postconditions to a set of RAC 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

Method Summary

abstract RacMethodDeclaration	createInternalMethod(AbstractMethodDeclaration meth) Creates an internal method for the given method.
abstract RacMethodDeclaration	createInternalMethod(MethodBinding meth) Creates an internal method for the given method.
abstract AbstractMethodDeclaration	createWrapperMethod(AbstractMethodDeclaration meth) Creates a wrapper method for the given method.
static MethodHeaderTranslator	forClass() Compilation unit of which methods to be translated.
static MethodHeaderTranslator	forInterface(TypeDeclaration sourceType)

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

Method Detail

forClass

public static MethodHeaderTranslator forClass()

Compilation unit of which methods to be translated.

forInterface

public static MethodHeaderTranslator forInterface(TypeDeclaration sourceType)

createInternalMethod

public abstract RacMethodDeclaration createInternalMethod(AbstractMethodDeclaration meth)

Creates an internal method for the given method. An internal method is a method to host the body of the given method which will be later turned into a wrapper method.

See Also:

createWrapperMethod(AbstractMethodDeclaration)

createInternalMethod

public abstract RacMethodDeclaration createInternalMethod(MethodBinding meth)

Creates an internal method for the given method. An internal method is a method to host the body of the given method which will be later turned into a wrapper method.

See Also:

createWrapperMethod(AbstractMethodDeclaration)

createWrapperMethod

public abstract AbstractMethodDeclaration createWrapperMethod(AbstractMethodDeclaration meth)

Creates a wrapper method for the given method. A wrapper method wraps assertion checking code around a call to the given method, which will be turned into an internal method.

See Also:

createInternalMethod(AbstractMethodDeclaration)