JML

org.jmlspecs.checker
Class JmlSigClassCreator

java.lang.Object
  extended byorg.multijava.mjc.ClassCreator
      extended byorg.jmlspecs.checker.JmlSigClassCreator

public class JmlSigClassCreator
extends ClassCreator

A concrete class creator to create JML classes from bytecode files.

Author:
Yoonsik Cheon

Field Summary
private static JmlSigClassCreator theInstance
          The unique instance of this class.
 
Constructor Summary
private JmlSigClassCreator()
          Creates a new instance.
 
Method Summary
 CBinaryField createBinaryField(CClass owner, FieldInfo fieldInfo)
          Creates a JML binary field object.
 CBinaryMethod createBinaryMethod(CClass owner, MethodInfo methodInfo, CClassContextType declCtx)
          Creates a JML binary method object.
 MemberAccess createMemberAccess(CClass owner, CMemberHost host, ClassInfo classInfo)
          Creates a JML member access object.
static ClassCreator getInstance()
          Returns the unique intance of this class.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

theInstance

private static final JmlSigClassCreator theInstance
The unique instance of this class.

Constructor Detail

JmlSigClassCreator

private JmlSigClassCreator()
Creates a new instance. This constructor is private to implement the Singleton design pattern.

Method Detail

createBinaryField

public CBinaryField createBinaryField(CClass owner,
                                      FieldInfo fieldInfo)
Creates a JML binary field object.

Overrides:
createBinaryField in class ClassCreator

createBinaryMethod

public CBinaryMethod createBinaryMethod(CClass owner,
                                        MethodInfo methodInfo,
                                        CClassContextType declCtx)
Creates a JML binary method object.

Overrides:
createBinaryMethod in class ClassCreator

createMemberAccess

public MemberAccess createMemberAccess(CClass owner,
                                       CMemberHost host,
                                       ClassInfo classInfo)
Creates a JML member access object.

Overrides:
createMemberAccess in class ClassCreator

getInstance

public static ClassCreator getInstance()
Returns the unique intance of this class.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.