Uses of Class
jml2b.structure.java.AClass

Packages that use AClass

jml2b.formula	Provides the classes necessary to create and manage formulas.
jml2b.link
jml2b.pog	Provides the classes necessary to generate proof obligations.
jml2b.pog.lemma
jml2b.pog.printers
jml2b.pog.util
jml2b.structure.bytecode
jml2b.structure.java
jml2b.structure.statement	Provides the classes necessary to create and manage java and jml statements and expressions.

Uses of AClass in jml2b.formula

Methods in jml2b.formula that return AClass

AClass

TTypeForm.getRefType()

Uses of AClass in jml2b.link

Fields in jml2b.link declared as AClass

AClass

LinkContext.currentClass

Methods in jml2b.link that return AClass

AClass

LinkContext.getCurrentClass()

Methods in jml2b.link with parameters of type AClass

void	LinkContext.setCurrentClass(AClass c)

Constructors in jml2b.link with parameters of type AClass

LinkContext(AClass ac)

Uses of AClass in jml2b.pog

Methods in jml2b.pog with parameters of type AClass

static SimpleLemma	Pog.declare(IJml2bConfiguration config, AClass c, java.util.Vector i) Quantifies and skolemizes the member invariant of a class for all instances of this class.
static Formula	Pog.quantify(IJml2bConfiguration config, AClass c, java.util.Vector i) Quantifies the member invariant of a class for all instances of this class.

Uses of AClass in jml2b.pog.lemma

Methods in jml2b.pog.lemma with parameters of type AClass

Proofs	ExceptionalBehaviourStack.throwException(java.lang.String vv, AClass c) Returns the proof obligation ensuring that the thrown of an exception ensures the current proof.
Proofs	ExceptionalBehaviourStack.throwException(IJml2bConfiguration config, AClass c) Calculates the proof obligation ensuring that the thrown of a runtime exception ensures the current proof.
Lemma	ExceptionalLemma.throwException(java.lang.String vv, AClass c)
boolean	ExceptionalLemma.catches(AClass c)
Lemma	ExsuresLemma.throwException(java.lang.String vv, AClass c)
boolean	ExsuresLemma.catches(AClass c)
Lemma	Lemma.throwException(java.lang.String vv, AClass c) Returns the lemma to prove to ensure that the thrown of an exception ensures the current lemma.
boolean	Lemma.catches(AClass c) Returns whether a exsures lemma catches a given exception.

Uses of AClass in jml2b.pog.printers

Methods in jml2b.pog.printers that return AClass

AClass

AClassEnumeration.nextElement()

Uses of AClass in jml2b.pog.util

Methods in jml2b.pog.util with parameters of type AClass

static int

IdentifierResolver.addIdent(AClass c) Adds a class identifier in the set of identifier.

Uses of AClass in jml2b.structure.bytecode

Subclasses of AClass in jml2b.structure.bytecode

class

ClassFile

Methods in jml2b.structure.bytecode that return AClass

AClass	ClassField.getDefiningClass()
AClass	ClassMethod.getDefiningClass()

Methods in jml2b.structure.bytecode with parameters of type AClass

AField

ClassFile.getField(java.lang.String name, AClass from)

Uses of AClass in jml2b.structure.java

Subclasses of AClass in jml2b.structure.java

class

Class Internal representation of classes.

Fields in jml2b.structure.java declared as AClass

AClass

Identifier.cl

Methods in jml2b.structure.java that return AClass

AClass	AClass.getSuperClass() Returns the super class of the current class.
AClass	Declaration.getDefiningClass() Returns the class that defines the declaration.
AClass	IType.getRefType()
static AClass	JmlLoader.loadClass(IJml2bConfiguration config, Package p, java.lang.String name) Returns the class name from package p.
static AClass	JmlLoader.loadClass(IJml2bConfiguration config, java.lang.String fqn) Load the given class, creating the package as needed.
AClass	Package.getClass(java.lang.String name) Search for the given class inside this package.
AClass	Package.getAndLoadClass(IJml2bConfiguration config, java.lang.String name) Return a reference to the class name.
AClass	Package.searchClass(java.lang.String s)
AClass	Type.getRefType() Returns the reference type for references or array types.
AClass	Type.getTargetedClass() Returns the class that is the type of the object or of the element of the type if it is an array.

Methods in jml2b.structure.java with parameters of type AClass

boolean	AClass.isSubclassOf(AClass super_class) Returns true if and only if super_class is a super class of this or if this and super_class are the same classes.
boolean	AClass.implementsInterface(AClass ith) Returns true if the current class implements the given interface.
abstract AField	AClass.getField(java.lang.String name, AClass from)
java.util.Vector	AClass.addSuperFields(AClass c, java.util.Vector v) Adds the fields defined by super classes that are visibles from the given class to the given vector.
AField	Class.getField(java.lang.String name, AClass from) Gets the field named name if it is visible from the given class.
void	Declaration.setDefiningClass(AClass c) Sets the class defining the declaration.
boolean	Declaration.isVisibleFrom(AClass c) Returns true if the declaration "this" is visible from the given class.
void	Package.addClass(AClass c)

Constructors in jml2b.structure.java with parameters of type AClass

Identifier(AClass c)
Creates a class identifier for the given class.

Type(AClass cl)
Creates a new type corresponding to the given class.

Uses of AClass in jml2b.structure.statement

Fields in jml2b.structure.statement declared as AClass

static AClass	Statement.nullPointerException The Class NullPointerException
static AClass	Statement.arrayIndexOutOfBoundsException The Class ArrayIndexOutOfBoundsException
static AClass	Statement.arithmeticException The Class ArithmeticException
static AClass	Statement.negativeArraySizeException The Class NegativeArraySizeException
static AClass	Statement.classCastException The Class ClassCastException
static AClass	Statement.arrayStoreException The Class ArrayStoreException