RacTranslator

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.jml4.rac
Class RacTranslator

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

All Implemented Interfaces:: RacConstants

Direct Known Subclasses:: MethodBodyTranslator, MethodHeaderTranslator, TypeDeclarationTranslator

public abstract class RacTranslator
extends java.lang.Object
implements RacConstants
extends java.lang.Object
implements RacConstants

Abstract superclass defining several utility methods for RAC translation.

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

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
`RacTranslator()`

Method Summary
`static java.lang.StringBuffer`	`argumentsToString(AbstractMethodDeclaration meth)` Returns the arguments of the given method as a comma-separated list of names.
`static java.lang.StringBuffer`	`argumentsToString(MethodBinding meth)` Returns the arguments of the given method as a comma-separated list of names.
`static ImportReference[]`	`createImportForRacRuntimePackage(CompilationUnitDeclaration cunit)` Creates and returns an import statement to import RAC tuntime package (`org.jmlspecs.jml4.rac.runtime`) if the given compilation unit doesn't import it; otherwise, returns null.
`static java.lang.String`	`escapeString(char[] val)` Returns a String formed by translating Unicode characters for the standard Java escape sequences into the corresponding escape sequences from JLS2, 3.10.6.
`static java.lang.String`	`escapeString(java.lang.String val)` Returns a String formed by translating Unicode characters for the standard Java escape sequences into the corresponding escape sequences from JLS2, 3.10.6.
`static java.lang.String`	`escapeString(java.lang.String val, boolean escapeApostrophes)` Returns a String formed by translating Unicode characters for the standard Java escape sequences into the corresponding escape sequences from JLS2, 3.10.6.
`static java.lang.String`	`getBoxedValue(TypeBinding binding, java.lang.String varName)` Returns a boxed value.
`static int`	`getCharacterNumber(int pos, CompilationResult cresult)` Given a compilation result, returns the character number of the given position counted in the line in which the character appears.
`static java.lang.String`	`getClassType(TypeBinding binding)` Return the class object of the given type.
`static char[]`	`getDeclaringClassName(AbstractMethodDeclaration meth)` Returns the name of the class that declaring the given method.
`static char[]`	`getDeclaringClassName(FieldBinding bind)` Returns the name of the class that declaring the given field.
`static java.lang.String`	`getDefaultValue(TypeBinding binding)` Returns the default value of the given type.
`static java.lang.StringBuffer`	`getErrorLocation(int pos, CompilationResult cresult)` Given a compilation result, returns the location information of a source position.
`static java.lang.String`	`getFullyQualifiedName(TypeBinding binding)` Returns the fully qualified name of the given type.
`static java.lang.String`	`getFullyQualifiedName(TypeReference ref)` Returns the fully qualified name of the given type.
`static int`	`getLineNumber(int pos, CompilationResult cresult)` Given a compilation result, returns the line number of the given position.
`static java.lang.StringBuffer`	`getRacErrorLocation(int pos, CompilationResult cresult)` Given a compilation result, returns the location information of a source position.
`static JmlMethodSpecification`	`getSpecification(AbstractMethodDeclaration meth)` Returns the specification of the given method or constructor.
`static java.lang.String`	`getUnboxedValue(TypeBinding binding, java.lang.String code)` Given code for a (boxed) expression of the given type, returns code that, if evaluated, will give the value boxed in the expression.
`static java.lang.String`	`getWrapperType(TypeBinding binding)` Given a primitive type, returns its wrapper type; otherwise, return `null`.
`static boolean`	`hasVoidReturnType(JmlMethodDeclaration meth)` Does the given method have void return type?
`static boolean`	`hasVoidReturnType(MethodBinding meth)` Does the given method have void return type?
`static boolean`	`isGhostField(FieldDeclaration field)` Is the given field a JML ghost field? A field is a JML ghost field if it has a `Ghost` annotation.
`static boolean`	`isModelField(FieldDeclaration field)` Is the given field a JML model field? A field is a JML model field if it has a `Model` annotation.
`static RacMethodDeclaration`	`makeMethod(java.lang.StringBuffer body, CompilationResult result)` Creates a method declaration with given body using the given compilation result.
`static RacMethodDeclaration`	`makeMethod(java.lang.String body, CompilationResult result)` Creates a method declaration with given body using the given compilation result.
`static RacMethodDeclaration`	`makeMethod(java.lang.String body, int modifiers, CompilationResult result)` Creates a method declaration with given body and modifiers using the given compilation result.
`static java.lang.StringBuffer`	`parameterDeclarationToString(AbstractMethodDeclaration meth)` Returns the formal parameter declaration of the given method as a string.
`static java.lang.StringBuffer`	`parameterDeclarationToString(MethodBinding meth)` Returns the formal parameter declaration of the given method as a string.
`static java.lang.StringBuffer`	`racErrorDeclaration(int tab, java.lang.String errorVar, java.lang.String stateVar)` Returns an indented code that declares two RAC variables used for reporting an assertion violation.
`static java.lang.StringBuffer`	`racErrorDefinition(int tab, java.lang.String errorVar, java.lang.String stateVar, int sourceStart, CompilationResult cresult, java.util.Collection<ASTNode> terms)` Returns an indented code that defines the values of two RAC variables used for reporting an assertion violation.
`static java.util.List<MethodDeclaration>`	`racMethodForName(TypeDeclaration type)` Creates RAC runtime methods for the given types.
`static java.util.List<MethodDeclaration>`	`racMethodsForGhostOrModel(TypeDeclaration type)` Returns a RAC runtime method for inheriting a ghost/model field.
`static java.util.List<MethodDeclaration>`	`racMethodsForSurrogate()`
`static java.util.List<MethodDeclaration>`	`racRuntimeMethods(TypeDeclaration type)` Creates RAC runtime methods for the given types.
`static java.lang.StringBuffer`	`throwsClauseToString(AbstractMethodDeclaration meth)` Returns the throws clause of the given method as a string.
`static java.lang.StringBuffer`	`throwsClauseToString(MethodBinding meth)` Returns the throws clause of the given method as a string.
`static java.lang.String`	`typeName(ReferenceBinding declaringClass)` Returns the type declaration name of `declaringClass`.
`static java.lang.String`	`typeName(TypeDeclaration typeDecl)` Returns the type declaration name of `typeDecl`.
`static java.lang.String`	`unescapeString(java.lang.String val)` Returns a String formed by translating Java escape sequences in the given String into single Unicode characters.

Methods inherited from class java.lang.Object
`equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Constructor Detail

RacTranslator

public RacTranslator()

Method Detail

makeMethod

public static RacMethodDeclaration makeMethod(java.lang.String body,
                                              CompilationResult result)

Creates a method declaration with given body using the given compilation result.

makeMethod

public static RacMethodDeclaration makeMethod(java.lang.StringBuffer body,
                                              CompilationResult result)

Creates a method declaration with given body using the given compilation result.

makeMethod

public static RacMethodDeclaration makeMethod(java.lang.String body,
                                              int modifiers,
                                              CompilationResult result)

Creates a method declaration with given body and modifiers using the given compilation result.

argumentsToString

public static java.lang.StringBuffer argumentsToString(AbstractMethodDeclaration meth)

Returns the arguments of the given method as a comma-separated list of names. If the method's parameters are

T1 x1, ..., Tn xn, the return value will be
 x1, ..., xn; an empty string is returned if the
 method have no parameter.





parameterDeclarationToString
public static java.lang.StringBuffer parameterDeclarationToString(AbstractMethodDeclaration meth)

Returns the formal parameter declaration of the given method as
 a string. The return value has the following the form:
 
   T1 x1, T2 x2, ..., Tn xn
 
 
 If the method has no parameter, an empty string is returned.











throwsClauseToString
public static java.lang.StringBuffer throwsClauseToString(AbstractMethodDeclaration meth)

Returns the throws clause of the given method as a string. 
 The return string has the following the form:
 
   throws E1, E2, ..., En
 
 
 If the method has no throws clause, an empty string is returned.











argumentsToString
public static java.lang.StringBuffer argumentsToString(MethodBinding meth)

Returns the arguments of the given method as a comma-separated
 list of names. If the method's parameters are 
 T1 x1, ..., Tn xn, the return value will be
 x1, ..., xn; an empty string is returned if the
 method have no parameter.











parameterDeclarationToString
public static java.lang.StringBuffer parameterDeclarationToString(MethodBinding meth)

Returns the formal parameter declaration of the given method as
 a string. The return value has the following the form:
 
   T1 x1, T2 x2, ..., Tn xn
 
 
 If the method has no parameter, an empty string is returned.











throwsClauseToString
public static java.lang.StringBuffer throwsClauseToString(MethodBinding meth)

Returns the throws clause of the given method as a string. 
 The return string has the following the form:
 
   throws E1, E2, ..., En
 
 
 If the method has no throws clause, an empty string is returned.











hasVoidReturnType
public static boolean hasVoidReturnType(MethodBinding meth)

Does the given method have void return type?











hasVoidReturnType
public static boolean hasVoidReturnType(JmlMethodDeclaration meth)

Does the given method have void return type?











isGhostField
public static boolean isGhostField(FieldDeclaration field)

Is the given field a JML ghost field? A field is a JML ghost field
 if it has a Ghost annotation.











isModelField
public static boolean isModelField(FieldDeclaration field)

Is the given field a JML model field? A field is a JML model field
 if it has a Model annotation.











getDeclaringClassName
public static char[] getDeclaringClassName(FieldBinding bind)

Returns the name of the class that declaring the given field.











getDeclaringClassName
public static char[] getDeclaringClassName(AbstractMethodDeclaration meth)

Returns the name of the class that declaring the given method.











getFullyQualifiedName
public static java.lang.String getFullyQualifiedName(TypeBinding binding)

Returns the fully qualified name of the given type.
 E.g., java.lang.Object.











getFullyQualifiedName
public static java.lang.String getFullyQualifiedName(TypeReference ref)

Returns the fully qualified name of the given type.
 E.g., java.lang.Object.











getDefaultValue
public static java.lang.String getDefaultValue(TypeBinding binding)

Returns the default value of the given type.











getBoxedValue
public static java.lang.String getBoxedValue(TypeBinding binding,
                                             java.lang.String varName)

Returns a boxed value. If the given variable (varName) 
 of the given type (binding) is of a primitive type,
 this methods returns a string representation of its boxed value;
 otherwise, it returns the variable.
 I.e., new java.lang.Integer(x) if 
 the variable x is the int type; 
 x if x is a reference type.











getUnboxedValue
public static java.lang.String getUnboxedValue(TypeBinding binding,
                                               java.lang.String code)

Given code for a (boxed) expression of the given type, returns code
 that, if evaluated, will give the value boxed in the expression.
 E.g., ((java.lang.Integer) code).intValue()
 for int and ((Sting) code)
 for String.











getClassType
public static java.lang.String getClassType(TypeBinding binding)

Return the class object of the given type.











getWrapperType
public static java.lang.String getWrapperType(TypeBinding binding)

Given a primitive type, returns its wrapper type; otherwise,
 return null. I.e., java.lang.Integer
 for int,











getCharacterNumber
public static int getCharacterNumber(int pos,
                                     CompilationResult cresult)

Given a compilation result, returns the character number of the given 
 position counted in the line in which the character appears.











getLineNumber
public static int getLineNumber(int pos,
                                CompilationResult cresult)

Given a compilation result, returns the line number of 
 the given position.











getErrorLocation
public static java.lang.StringBuffer getErrorLocation(int pos,
                                                      CompilationResult cresult)

Given a compilation result, returns the location information 
 of a source position. The return string will have the following
 form:
 
   File: MyClass.java Line: 10 Character: 20
 











getRacErrorLocation
public static java.lang.StringBuffer getRacErrorLocation(int pos,
                                                         CompilationResult cresult)

Given a compilation result, returns the location information 
 of a source position. The return string will have the following
 form:
 
   new JMLAssertionError.location("MyClass.java", 10, 20)
 











getSpecification
public static JmlMethodSpecification getSpecification(AbstractMethodDeclaration meth)

Returns the specification of the given method or constructor.











racMethodForName
public static java.util.List<MethodDeclaration> racMethodForName(TypeDeclaration type)

Creates RAC runtime methods for the given types. The result list 
 has rac$forName method.











racRuntimeMethods
public static java.util.List<MethodDeclaration> racRuntimeMethods(TypeDeclaration type)

Creates RAC runtime methods for the given types. If the given 
 type allows static methods, the created methods are static;
 otherwise, non-static methods are created. The result list 
 includes the following methods.
 
 
  rac$receiver
  
  
rac$check
 











racMethodsForSurrogate
public static java.util.List<MethodDeclaration> racMethodsForSurrogate()











racMethodsForGhostOrModel
public static java.util.List<MethodDeclaration> racMethodsForGhostOrModel(TypeDeclaration type)

Returns a RAC runtime method for inheriting a ghost/model field.
 The returned method assumes the existence of RAC runtime methods
 created by racRuntimeMethods(TypeDeclaration).











racErrorDeclaration
public static java.lang.StringBuffer racErrorDeclaration(int tab,
                                                         java.lang.String errorVar,
                                                         java.lang.String stateVar)

Returns an indented code that declares two RAC variables used for 
 reporting an assertion violation. The returned code has the 
 following form:
 
   java.util.Set errorVar = new java.util.HashSet();
  java.util.Map stateVar
    = new java.util.HashMap();
 











racErrorDefinition
public static java.lang.StringBuffer racErrorDefinition(int tab,
                                                        java.lang.String errorVar,
                                                        java.lang.String stateVar,
                                                        int sourceStart,
                                                        CompilationResult cresult,
                                                        java.util.Collection<ASTNode> terms)

Returns an indented code that defines the values of two RAC 
 variables used for reporting an assertion violation. The returned 
 code has the following form:
 
   errorVar.add(new JMLAssertionError.Location("X.java", 4, 14));
  stateVar.put("x1", x1);
  ...
  stateVar.put("xn", xn);
 
 
 where the error location is calculating using sourceStar
 and cresult, and each xi is a node 
 contained in terms.











createImportForRacRuntimePackage
public static ImportReference[] createImportForRacRuntimePackage(CompilationUnitDeclaration cunit)

Creates and returns an import statement to import RAC tuntime package
 (org.jmlspecs.jml4.rac.runtime) if the given compilation
 unit doesn't import it; otherwise, returns null.











unescapeString
public static final java.lang.String unescapeString(java.lang.String val)

Returns a String formed by translating Java escape sequences in
 the given String into single Unicode characters.  The escape
 sequences are those of JLS2, 3.10.6 with the addition of
 Unicode escapes.





See Also:
escapeString(String)





escapeString
public static final java.lang.String escapeString(java.lang.String val)

Returns a String formed by translating Unicode characters for
 the standard Java escape sequences into the corresponding
 escape sequences from JLS2, 3.10.6.  Octal and unicode escapes
 are not generated.





See Also:
escapeString(String,boolean), 
unescapeString(String)





escapeString
public static final java.lang.String escapeString(char[] val)

Returns a String formed by translating Unicode characters for
 the standard Java escape sequences into the corresponding
 escape sequences from JLS2, 3.10.6.  Octal and unicode escapes
 are not generated.





See Also:
escapeString(String,boolean), 
unescapeString(String)





escapeString
public static final java.lang.String escapeString(java.lang.String val,
                                                  boolean escapeApostrophes)

Returns a String formed by translating Unicode characters for
 the standard Java escape sequences into the corresponding
 escape sequences from JLS2, 3.10.6.  Octal and unicode escapes
 are not generated.





See Also:
unescapeString(String)





typeName
public static java.lang.String typeName(TypeDeclaration typeDecl)

Returns the type declaration name of typeDecl. It returns
 the simple name of the type preceded by the package name.





Parameters:
typeDecl - 
Returns:
String





typeName
public static java.lang.String typeName(ReferenceBinding declaringClass)

Returns the type declaration name of declaringClass. It 
 returns the simple name of the type preceded by the package name.





Parameters:
typeDecl - 
Returns:
String














  
      Overview 
      Package 
    Class 
      Use 
      Tree 
      Deprecated 
      Index 
      Help 
  









 PREV CLASS 
 NEXT CLASS

  FRAMES   
 NO FRAMES   
 







  SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.jml4.rac Class RacTranslator

RacTranslator

makeMethod

makeMethod

makeMethod

argumentsToString

parameterDeclarationToString

throwsClauseToString

argumentsToString

parameterDeclarationToString

throwsClauseToString

hasVoidReturnType

hasVoidReturnType

isGhostField

isModelField

getDeclaringClassName

getDeclaringClassName

getFullyQualifiedName

getFullyQualifiedName

getDefaultValue

getBoxedValue

getUnboxedValue

getClassType

getWrapperType

getCharacterNumber

getLineNumber

getErrorLocation

getRacErrorLocation

getSpecification

racMethodForName

racRuntimeMethods

racMethodsForSurrogate

racMethodsForGhostOrModel

racErrorDeclaration

racErrorDefinition

createImportForRacRuntimePackage

unescapeString

escapeString

escapeString

escapeString

typeName

typeName

org.jmlspecs.jml4.rac
Class RacTranslator