org.jmlspecs.jml4.rac
Class WrapperMethodGenerator

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

Direct Known Subclasses:

WrapperConstructorGenerator

public class WrapperMethodGenerator
extends java.lang.Object

Generates a wrapper method. A wrapper method is a method with the same name and signature as the method under translation, and thus it replaces the method; the method under translation is turned into a private internal method. A wrapper method forwards an incoming call to the internal method but wrapped with various assertion checks before and after the call forwarding and has the following general structure:

  T m(T1 x1, ..., Tn xn) throws E1, ..., En {
    evalOldExprInHC$static();
    checkInv$static();
    checkInv$instance$S();
    checkPre$m$S(x1, ..., xn);
    
    boolean rac$ok = true;
    try {
      [rac$result =] internal$m(x1, ..., xn);
      checkPost$m$S(x1, ..., xn [, rac$result]);
    } catch (JMLPreconditionError e) {
      rac$ok = false;
      throw new JMLInternalPreconditionError(e);
    } catch (JMLNormalPostconditionError e) {
        rac$ok = false;
        throw new JMLInternalNormalPostconditionError(e);
    } catch (JMLExceptionalPostconditionError e) {
        rac$ok = false;
      throw new JMLInternalExceptionalPostconditionError(e);
    } catch (JMLAssertionError rac$er) {
        rac$ok = false;
      throw rac$er;
    } catch (Throwable e) {
      try {
        checkXPost$m$S(x1, ..., xn, e);
      } catch (JMLAssertionError rac$er) {
        rac$ok = false;
        throw rac$er;
      }
    } finally {
        if (rac$ok) {
           checkInv$static();
           checkInv$instance$S();
      }
    }
  }
 

Author:

Amritam Sarcar and Yoonsik Cheon

Constructor Summary

WrapperMethodGenerator()
Creates a new wrapper generator.

Method Summary

MethodDeclaration	generate(AbstractMethodDeclaration cmeth) Generates and returns a wrapper method for the given method.
static java.lang.StringBuffer	headerToString(AbstractMethodDeclaration meth) Returns the string representation of the header of the given method.
boolean	isHelperMethod(AbstractMethodDeclaration cmeth)

Methods inherited from class java.lang.Object

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

Constructor Detail

WrapperMethodGenerator

public WrapperMethodGenerator()

Creates a new wrapper generator.

Method Detail

headerToString

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

Returns the string representation of the header of the given method. The return value has the following form:

  public T0 m(T1 x1, ..., Tn Xn) throws E1, ..., En
  

generate

public MethodDeclaration generate(AbstractMethodDeclaration cmeth)

Generates and returns a wrapper method for the given method. The wrapper method is stored in the racCode field of the returned method except for its modifiers which is available from the modifiers field of the returned method.

isHelperMethod

public boolean isHelperMethod(AbstractMethodDeclaration cmeth)