org.jmlspecs.jmlrac
Class DesugarSpec

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.checker.JmlAbstractVisitor
          org.jmlspecs.jmlrac.DesugarSpec

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor

public class DesugarSpec

extends JmlAbstractVisitor

implements JmlVisitor

A JML visitor class for desugaring method specifications. In the desugared form, a generic specification, a normal behavior specification and a exceptional specification are all translated into a (general form of) behavior specification. A case-analysis specification, known as specification cases, and a nested specification are also desugared. The desugaring does not produce a completely desugared method specification, but a partial form sufficient for the further processing by the runtime assertion checker.

In the desugared specification, each specification case is translated into a general behavior specification case. If necessary, a default specification body clause such as ensures clause and signals clause is added. A specification cases specification is desugared by copying specificification variable declarations and specification headers into each specification case. A nested specification is desugared by unfolding the nesting. For example, the following specification:

  also requires p1; {| ensures p2; also ensures p3; |}
  also behavior ensures p4;
  also normal_behavior ensures p5;
  also exceptional_behavior signals (E e) p6;
 

  also behavior requires p1; ensures p2;
  also behavior requires p1; ensures p3;
  also behavior ensures p4;
  also behavior ensures p5; signals (Exception e) false;
  also behavior signals (E e) p6; ensures false;
 

Field Summary
private  CClassType[]	exceptions           Exceptions that the target method may throw.
private  boolean	heavyweight           True iff the current specification being desugared is heavyweight.
private  Stack	resultStack           for passing results (return values) between visitor methods.

 

Fields inherited from class org.multijava.util.Utils

DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO

 

Fields inherited from interface org.jmlspecs.checker.Constants

ACC2_RAC_METHOD, ACC_CODE, ACC_CODE_BIGINT_MATH, ACC_CODE_JAVA_MATH, ACC_CODE_SAFE_MATH, ACC_GHOST, ACC_HELPER, ACC_INSTANCE, ACC_MODEL, ACC_MONITORED, ACC_QUERY, ACC_SECRET, ACC_SPEC_BIGINT_MATH, ACC_SPEC_JAVA_MATH, ACC_SPEC_PROTECTED, ACC_SPEC_PUBLIC, ACC_SPEC_SAFE_MATH, ACC_UNINITIALIZED, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_BIGINT_MATH, EVERYTHING, JML_JMLObjectSet, NOT_SPECIFIED, NOTHING, OPE_BACKWARD_IMPLIES, OPE_EQUIV, OPE_EXISTS, OPE_FORALL, OPE_IMPLIES, OPE_L_ARROW, OPE_MAX, OPE_MIN, OPE_NOT_EQUIV, OPE_NUM_OF, OPE_PRODUCT, OPE_R_ARROW, OPE_SUBTYPE, OPE_SUM, SAME, TID_BIGINT, TID_REAL, TID_TYPE, TN_JMLOBJECTSET, TN_JMLTYPE, TN_JMLVALUESET

 

Fields inherited from interface org.multijava.mjc.Constants

ACC_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, NULLITY_MODS, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP

 

Fields inherited from interface org.multijava.util.classfile.Constants

ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_SYNTHETIC, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID

 

Constructor Summary

DesugarSpec()           Constructs a new instance.

 

Method Summary
private  JmlGenericSpecCase	add(JmlGenericSpecCase specCase, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader)           Adds the given spec var decls, specVarDecls, and spec header, specHeader, to the spec case, specCase.
private  JmlBehaviorSpec	addDefaultRequiresClause(JmlBehaviorSpec bs)           Adds a default requires clause to the given behaviorSpec, bs, and returns it.
protected  JmlEnsuresClause	defaultEnsuresClause(TokenReference where)           Returns a default ensures clause for an exceptional specification.
protected  JmlRequiresClause	defaultRequiresClause(TokenReference where)           Returns a default requires clause for an behavior spec case.
private  JmlSignalsClause	defaultSignalsClause(TokenReference where)           Returns a default signals clause for a normal specification.
private  JmlSignalsClause	defaultSignalsClause(TokenReference where, CClassType[] exceptions)           Returns a default signals clause for a lightweight specification whose method may throw the given exceptions.
private  Object	GET_RESULT()           Pops and returns the top element of the result stack.
JmlMethodSpecification	perform(JmlMethodSpecification mspec, CClassType[] exceptions)           Returns a desugared specification of the given method specification.
private  void	RETURN_RESULT(Object obj)           Pushes the argument to the result stack.
private  void	visitHeavyweightSpec(JmlHeavyweightSpec self)           Desugars a general/normal/exceptional behavior specification.
void	visitJmlBehaviorSpec(JmlBehaviorSpec self)           Desugars a behavior specification.
void	visitJmlExceptionalBehaviorSpec(JmlExceptionalBehaviorSpec self)           Desugars an exceptional behavior specification.
void	visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)           Desugars an exceptional specification body.
void	visitJmlExceptionalSpecCase(JmlExceptionalSpecCase self)           Desugars an exceptional specification case.
void	visitJmlExtendingSpecification(JmlExtendingSpecification self)           Desugar an extending specification.
void	visitJmlGenericSpecBody(JmlGenericSpecBody self)           Desugars a generic specification body.
void	visitJmlGenericSpecCase(JmlGenericSpecCase self)           Desugars a generic specification case.
void	visitJmlNormalBehaviorSpec(JmlNormalBehaviorSpec self)           Desugars a normal behavior specification.
void	visitJmlNormalSpecBody(JmlNormalSpecBody self)           Desugars a normal specification body.
void	visitJmlNormalSpecCase(JmlNormalSpecCase self)           Desugars a normal specification case.
void	visitJmlSpecification(JmlSpecification self)           Desugars the given JML specification.
private  void	visitSpecBody(JmlSpecBody self, JmlSpecBodyClause body)           Desugars a specification body (general, normal, exceptional).
private  void	visitSpecCase(JmlGeneralSpecCase self)           Desugars a specification case (general, normal, exceptional).
private  void	visitSpecification(JmlSpecification self)           Desugars a JML specification or an OR-extending specification.

 

Methods inherited from class org.jmlspecs.checker.JmlAbstractVisitor

visitAddExpression, visitArrayAccessExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssertStatement, visitAssignmentExpression, visitBinaryExpression, visitBitwiseExpression, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitByteLiteral, visitCastExpression, visitCatchClause, visitCharLiteral, visitClassBlock, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitCompoundStatement, visitCompoundStatement, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDivideExpression, visitDoStatement, visitDoubleLiteral, visitEmptyStatement, visitEqualityExpression, visitExplicitConstructorInvocation, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFieldExpression, visitFloatLiteral, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceDeclaration, visitIntLiteral, visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlElemTypeExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalExample, visitJmlExpression, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlFreshExpression, visitJmlGeneralSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalExpression, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantForExpression, visitJmlInvariantStatement, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLetVarDecl, visitJmlLockSetExpression, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMaxExpression, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNonNullElementsExpression, visitJmlNormalExample, visitJmlNotAssignedExpression, visitJmlNotModifiedExpression, visitJmlOldExpression, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicate, visitJmlPredicateKeyword, visitJmlPreExpression, visitJmlReachExpression, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRelationalExpression, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlResultExpression, visitJmlReturnsClause, visitJmlSetComprehension, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecExpression, visitJmlSpecQuantifiedExpression, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlTypeExpression, visitJmlTypeOfExpression, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion, visitLabeledStatement, visitLocalVariableExpression, visitLongLiteral, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitNewObjectExpression, visitNullLiteral, visitOrdinalLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitPostfixExpression, visitPrefixExpression, visitRealLiteral, visitRelationalExpression, visitReturnStatement, visitShiftExpression, visitShortLiteral, visitStringLiteral, visitSuperExpression, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThisExpression, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitTypeNameExpression, visitUnaryExpression, visitUnaryPromoteExpression, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement

 

Methods inherited from class org.multijava.util.Utils

assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray

 

Methods inherited from class java.lang.Object

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

 

Methods inherited from interface org.jmlspecs.checker.JmlVisitor

visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlElemTypeExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalExample, visitJmlExpression, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlFreshExpression, visitJmlGeneralSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalExpression, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantForExpression, visitJmlInvariantStatement, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLetVarDecl, visitJmlLockSetExpression, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMaxExpression, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNonNullElementsExpression, visitJmlNormalExample, visitJmlNotAssignedExpression, visitJmlNotModifiedExpression, visitJmlOldExpression, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicate, visitJmlPredicateKeyword, visitJmlPreExpression, visitJmlReachExpression, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRelationalExpression, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlResultExpression, visitJmlReturnsClause, visitJmlSetComprehension, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecExpression, visitJmlSpecQuantifiedExpression, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlTypeExpression, visitJmlTypeOfExpression, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion

 

Methods inherited from interface org.multijava.mjc.MjcVisitor

visitAddExpression, visitArrayAccessExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssertStatement, visitAssignmentExpression, visitBitwiseExpression, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitCastExpression, visitCatchClause, visitCharLiteral, visitClassBlock, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitCompoundStatement, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDivideExpression, visitDoStatement, visitEmptyStatement, visitEqualityExpression, visitExplicitConstructorInvocation, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFieldExpression, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceDeclaration, visitLabeledStatement, visitLocalVariableExpression, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitNewObjectExpression, visitNullLiteral, visitOrdinalLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitPostfixExpression, visitPrefixExpression, visitRealLiteral, visitRelationalExpression, visitReturnStatement, visitShiftExpression, visitStringLiteral, visitSuperExpression, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThisExpression, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitTypeNameExpression, visitUnaryExpression, visitUnaryPromoteExpression, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement

 

Field Detail

resultStack

private Stack resultStack

for passing results (return values) between visitor methods.

See Also:

GET_RESULT(), RETURN_RESULT(Object)

exceptions

private CClassType[] exceptions

Exceptions that the target method may throw.

heavyweight

private boolean heavyweight

True iff the current specification being desugared is heavyweight.

DesugarSpec

public DesugarSpec()

Constructs a new instance.

perform

public JmlMethodSpecification perform(JmlMethodSpecification mspec,
                                      CClassType[] exceptions)

Returns a desugared specification of the given method specification.

Parameters:

mspec - the method specification to be desugared

exceptions - exceptions that the target method may throw.

Returns:

the desugared method specification

See Also:

visitJmlSpecification(JmlSpecification)

visitJmlSpecification

public void visitJmlSpecification(JmlSpecification self)

Desugars the given JML specification. In the desugared specification, each specification case is translated into a general behavior specification case. A default specification body clause such as ensures clause and signals clause is added if necessary. A specification cases specification is desugared by copying specificification variable declarations and specification headers into each specification case. A nested specification is desugared by unfolding the nesting. For example, the following specification:

  also requires p1; {| ensures p2; also ensures p3; |}
  also behavior ensures p4;
  also normal_behavior ensures p5;
  also exceptional_behavior signals (E e) p6;
 

is desugared into:

  also behavior requires p1; ensures p2;
  also behavior requires p1; ensures p3;
  also behavior ensures p4;
  also behavior ensures p5; signals (Exception e) false;
  also behavior signals (E e) p6; ensures false;
 

Both the subclassing contract and redundant specifications are not desugared.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlSpecification in interface JmlVisitor

Overrides:

visitJmlSpecification in class JmlAbstractVisitor

visitSpecification

private void visitSpecification(JmlSpecification self)

Desugars a JML specification or an OR-extending specification.

 requires self != null && resultStack != null;
 requires (self instanceof JmlSpecification) ||
    (* self is an OR-extending specification *);
 assignable resultStack;
 ensures resultStack.size() == \old(resultStack.size() + 1);
 

addDefaultRequiresClause

private JmlBehaviorSpec addDefaultRequiresClause(JmlBehaviorSpec bs)

Adds a default requires clause to the given behaviorSpec, bs, and returns it.

visitJmlExtendingSpecification

public void visitJmlExtendingSpecification(JmlExtendingSpecification self)

Desugar an extending specification. In the desugared specification, each conjoinable specification is translated into a corresponding behavior conjoinable specification, if necssary, with a default specification body clause added. For example, the method specification of:

  and ensures p1; 
  and behavior ensures p2;
  and normal_behavior ensures p3;
  and exceptional_behavior signals (E e) p4;
 

is desugared into:

  and behavior ensures p1;
  and behavior ensures p2;
  and behavior ensures p3; signals (Exception e) false;
  and behavior signals (E e) p4; ensures false;
 

Redundant specifications are not desugared.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlExtendingSpecification in interface JmlVisitor

Overrides:

visitJmlExtendingSpecification in class JmlAbstractVisitor

visitJmlBehaviorSpec

public void visitJmlBehaviorSpec(JmlBehaviorSpec self)

Desugars a behavior specification.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlBehaviorSpec in interface JmlVisitor

Overrides:

visitJmlBehaviorSpec in class JmlAbstractVisitor

visitJmlNormalBehaviorSpec

public void visitJmlNormalBehaviorSpec(JmlNormalBehaviorSpec self)

Desugars a normal behavior specification.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlNormalBehaviorSpec in interface JmlVisitor

Overrides:

visitJmlNormalBehaviorSpec in class JmlAbstractVisitor

visitJmlExceptionalBehaviorSpec

public void visitJmlExceptionalBehaviorSpec(JmlExceptionalBehaviorSpec self)

Desugars an exceptional behavior specification.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlExceptionalBehaviorSpec in interface JmlVisitor

Overrides:

visitJmlExceptionalBehaviorSpec in class JmlAbstractVisitor

visitJmlGenericSpecCase

public void visitJmlGenericSpecCase(JmlGenericSpecCase self)

Desugars a generic specification case.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlGenericSpecCase in interface JmlVisitor

Overrides:

visitJmlGenericSpecCase in class JmlAbstractVisitor

visitJmlGenericSpecBody

public void visitJmlGenericSpecBody(JmlGenericSpecBody self)

Desugars a generic specification body.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlGenericSpecBody in interface JmlVisitor

Overrides:

visitJmlGenericSpecBody in class JmlAbstractVisitor

visitJmlNormalSpecCase

public void visitJmlNormalSpecCase(JmlNormalSpecCase self)

Desugars a normal specification case.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlNormalSpecCase in interface JmlVisitor

Overrides:

visitJmlNormalSpecCase in class JmlAbstractVisitor

visitJmlNormalSpecBody

public void visitJmlNormalSpecBody(JmlNormalSpecBody self)

Desugars a normal specification body.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlNormalSpecBody in interface JmlVisitor

Overrides:

visitJmlNormalSpecBody in class JmlAbstractVisitor

visitJmlExceptionalSpecCase

public void visitJmlExceptionalSpecCase(JmlExceptionalSpecCase self)

Desugars an exceptional specification case.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlExceptionalSpecCase in interface JmlVisitor

Overrides:

visitJmlExceptionalSpecCase in class JmlAbstractVisitor

visitJmlExceptionalSpecBody

public void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)

Desugars an exceptional specification body.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visitJmlExceptionalSpecBody in interface JmlVisitor

Overrides:

visitJmlExceptionalSpecBody in class JmlAbstractVisitor

visitHeavyweightSpec

private void visitHeavyweightSpec(JmlHeavyweightSpec self)

Desugars a general/normal/exceptional behavior specification.

 requires self != null && resultStack != null;
 assignable resultStack;
 assignable_redundantly heavyweight;
 ensures resultStack.size() == \old(resultStack.size() + 1);
 

defaultRequiresClause

protected JmlRequiresClause defaultRequiresClause(TokenReference where)

Returns a default requires clause for an behavior spec case.

 requires where != null;
 ensures \result != null;
 

defaultSignalsClause

private JmlSignalsClause defaultSignalsClause(TokenReference where)

Returns a default signals clause for a normal specification. The returned signals clause has the form: signals (Exception e) false.

 requires where != null;
 ensures \result != null;
 

defaultSignalsClause

private JmlSignalsClause defaultSignalsClause(TokenReference where,
                                              CClassType[] exceptions)

Returns a default signals clause for a lightweight specification whose method may throw the given exceptions. The returned signals clause has the form:

  signals (Throwable e) e instanceof E1 || ... || e instanceof En;
 

defaultEnsuresClause

protected JmlEnsuresClause defaultEnsuresClause(TokenReference where)

Returns a default ensures clause for an exceptional specification.

 requires where != null;
 ensures \result != null;
 

visitSpecCase

private void visitSpecCase(JmlGeneralSpecCase self)

Desugars a specification case (general, normal, exceptional).

 requires self != null && resultStack != null;
 assignable resultStack;
 ensures resultStack.size() == \old(resultStack.size() + 1);
 

visitSpecBody

private void visitSpecBody(JmlSpecBody self,
                           JmlSpecBodyClause body)

Desugars a specification body (general, normal, exceptional).

 requires self != null && resultStack != null;
 assignable resultStack;
 ensures resultStack.size() == \old(resultStack.size() + 1);
 

add

private JmlGenericSpecCase add(JmlGenericSpecCase specCase,
                               JmlSpecVarDecl[] specVarDecls,
                               JmlRequiresClause[] specHeader)

Adds the given spec var decls, specVarDecls, and spec header, specHeader, to the spec case, specCase.

GET_RESULT

private Object GET_RESULT()

Pops and returns the top element of the result stack.

 requires resultStack != null;
 assignable resultStack;
 ensures resultStack != null;
 

RETURN_RESULT

private void RETURN_RESULT(Object obj)

Pushes the argument to the result stack.

 requires obj != null && resultStack != null;
 assignable resultStack;
 ensures resultStack != null;