C. Code Examples

C.1 Unreachable Post Condition Code in iContract

This appendix shows, that iContract cannot handle methods with an unreachable end of method body as stated in section .

The example is derived from the example code that accompanies iContract. The following method provides such a situation: The throw statement in the last line prevents the execution path from ever reaching the end of the method body.

/**
 * @post age > 0
 */
public void setAge( int age )
{ 
  age_ = age;
  throw new RuntimeException();
}

Now the post condition has to be included into iContracts configuration, so that it actually gets checked.

iContract.doc.tutorial.Person.Employee.setAge(int) post

Now iContract performs the instrumentation of source code. When trying to compile the instrumented code, the compiler fails:

Employee.java:166: Statement not reached.
/*|*/ try {

To see why, let's have a look at the instrumented code.

/**
 * @post age > 0
 */

public void setAge(int age )
{
  /*|*/ //#*#-------------------
  /*|*/ [ shorted by the author]
  /*|*/ //-------------------#*#
  /*|*/ try {
  /*|*/ //--------------------
  /*|*/
   age_ = age;
   throw new RuntimeException();
  /*|*/ //#*#-------------------
  /*|*/ try { <- line 166 is here
  /*|*/ if (!(age > 0))
  /*|*/   [ shortened by the author ]
  /*|*/     }
  /*|*/ catch ( RuntimeException ex ) {
  /*|*/ [ shortened by the author ] }
  /*|*/
  /*|*/ //------------------#*#
  /*|*/ 
  /*|*/ //#*#------------------
  /*|*/ } finally {
  /*|*/ [ shortened by the author ]
  /*|*/ }

  /*|*/ //------------------#*#
  /*|*/
}

The original code fragment is followed by generated code checking the post condition. Since this code isn't reachable, the java compiler fails.

C.2 Return Opcodes in Java Byte Code

This appendix lists the example used to verify the statement of section , that byte code instrumentation does not need control flow analysis when inserting post method code.

The end of method body below isn't a reachable point of code.

void method1() 
{ 
  throw new RuntimeException(); 
}

Thus, the end of the compiled method does not have a return opcode.

Method void method1() 
0 new #10 <Class java.lang.RuntimeException> 
3 dup 
4 invokespecial #14 <Method java.lang.RuntimeException()> 
7 athrow 

The end of the second method is a reachable point of code.

void method2() 
{
} 

Accordingly, the method ends with a return opcode, even if the source code did not contain a return statement.

Method void method2() 
0 return 

Disassembling was done with javap -c.

C.3 The Problem with Versant Database

This appendix shows why the Versant ODBMS and the Dresden OCL Toolkit don't work together.

The problem is a bug in Java Versant Interface [VC] (JVI). JVI provides an enhancer, which instruments the user application on byte code level. The enhancer transforms any access to object fields into a call to a wrapper method provided by JVI.

The class used for invariant caching must be database persistent. Thus, it also has to be enhanced. This class contains the following piece of source code.

Field f=...;
if(f==null)
  throw new RuntimeException(...);
f.setAccessible(true);
HashSet observer=(HashSet)(f.get(o));  

The last line is Invariant.java:69. This line throws the exception shown below.

java.lang.NoSuchMethodException:
_vj_getfield_com_net_linx_iyp_businessObject_InColumnAd_startOnline
at com.versant.trans.Wrappers.method_invoke
  (Wrappers.java:209)
at com.versant.trans.Wrappers.java_lang_reflect_Field_get_internal
  (Wrappers.java:344)
at com.versant.trans.Wrappers.java_lang_reflect_Field_get
  (Wrappers.java:369)
at tudresden.ocl.injection.lib.Invariant.addObserver
  (Invariant.java:69)
...

The code line in question contains a method call to Field.get. This method cannot throw a NoSuchMethodException under normal circumstances.

What happened? The enhancer transformed the call to Field.get into a call to a wrapper method provided by JVI. This method probably does some database stuff, and then tries to access the field requested. Therefore it tries to invoke another wrapper method _vj_getfield_com_net_linx_iyp_businessObject_InColumnAd_startOnline on the object. The class of the object is InColumnAd, the field requested is startOnline. However, this method does not exist, since the field is inherited from its super class.

This bug prevents any code from accessing object fields via reflection, if the objects class inherits this field from a super class. This affects the runtime libraries of both the OCL code generator and the code instrumentation.

A possible work-around is to wrap all field accesses with corresponding methods. These methods would access their field without reflection, thus would not be affected by the bug. These methods could be created automatically by the OCL code instrumentation. This would require a moderate implementation effort. However, the design of the OCL toolkit would suffer a much tighter dependency between the OCL library and the code instrumentation. The author does not plan to implement this work-around.

On October 13, 2000 Versant support announced a bugfix ``available within the next few weeks.'' After submission of this paper, on February 27, 2001 this bugfix was published as patch bundle 3 for JVI 2.4.0 on Linux.