Package daikon.tools.jtb

Class Annotation

Object

Annotation

public class Annotation
extends Object

Utility class to parse annotations generated with the Annotate program using the --wrap_xml flag.

An example of the String representation of an annotation, as output with the --wrap_xml flag, is:

 <INVINFO>
 <INV> this.topOfStack <= this.theArray.length-1 </INV>
 <ENTER>
 <DAIKON>  this.topOfStack <= size(this.theArray[])-1  </DAIKON>
 <DAIKONCLASS>class daikon.inv.binary.twoScalar.IntLessEqual</DAIKONCLASS>
 <METHOD>  isEmpty()  </METHOD>
 </INVINFO>
 

The above string should actually span only one line.

To be well-formed, an annotation should be enclosed in <INVINFO> tags, contain

 <DAIKON> and
 <METHOD>
 

tags, and exactly one of

 <ENTER>,
 <EXIT>,
 <OBJECT>, or
 <CLASS>.
 

Obviously, the tool Annotate outputs well-formed annotations, so the user shouldn't have to worry too much about well-formedness.

Two annotations are equal iff their fields "daikonRep", "method" and "kind" are equal.

The factory method get(String annoString) returns an annotation that equals to the annotation represented by annoString. In particular, if the same String is given twice to get(String annoString), the method will return the same Annotation object.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	Annotation.Kind	A class representing the kind of an annotation.
static class	Annotation.MalformedAnnotationException	Thrown by method get(String annoString) if annoString doesn't represent a well-formed annotation.

Field Summary

Fields

Modifier and Type	Field	Description
String	daikonClass

Method Summary

Modifier and Type	Method	Description
String	daikonClass()	The Daikon class name that this invariant represents an instance of.
String	daikonRep()	The way this annotation would be printed by Daikon.
boolean	equals(@GuardSatisfied @Nullable Object o)	Two annotations are equal iff their fields "daikonRep", "method" and "kind" are equal.
static Annotation[]	findAnnotations(String annoString)	Find, parse and return all distinct annotations found in a String.
static Annotation[]	findAnnotations(List<String> annoStrings)	Find, parse and return all distinct annotations found in a list of strings.
static Annotation	get(Annotation.Kind kind, String daikonRep, String method, String invRep, String daikonClass)	Get the annotation with corresponding properties.
static Annotation	get(String annoString)	Parse a String and return the annotation that it represents.
int	hashCode()
String	invRep()	Representation of this annotation (the format depends on which output format was used to create the annotation in Daikon; it's one of JAVA, JML, ESC or DBC).
Annotation.Kind	kind()	The kind of this annotation.
String	method()	The method that this annotation refers to.
String	toString()	Easy-on-the-eye format.
String	xmlString()	XML representation.

Methods inherited from class Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

daikonClass

public String daikonClass

Method Detail

daikonRep

public String daikonRep(@GuardSatisfied Annotation this)

The way this annotation would be printed by Daikon.

method

public String method(@GuardSatisfied Annotation this)

The method that this annotation refers to.

kind

public Annotation.Kind kind(@GuardSatisfied Annotation this)

The kind of this annotation.

invRep

public String invRep()

Representation of this annotation (the format depends on which output format was used to create the annotation in Daikon; it's one of JAVA, JML, ESC or DBC).

daikonClass

public String daikonClass()

The Daikon class name that this invariant represents an instance of.

get

public static Annotation get(String annoString)
                      throws Annotation.MalformedAnnotationException

Parse a String and return the annotation that it represents.

Throws:

Annotation.MalformedAnnotationException

xmlString

public String xmlString()

XML representation. May be different from the String used to generate the input; only those tags that were parsed by the get() method will be output here.

findAnnotations

public static Annotation[] findAnnotations(String annoString)

Find, parse and return all distinct annotations found in a String. The string annoString may contain none, one, or several annotations. Malformed annotations are ignored.

findAnnotations

public static Annotation[] findAnnotations(List<String> annoStrings)

Find, parse and return all distinct annotations found in a list of strings. Each string in annoStrings may contain none, one, or several annotations. Malformed annotations are ignored.

toString

@SideEffectFree
public String toString(@GuardSatisfied Annotation this)

Easy-on-the-eye format.

Overrides:

toString in class Object

equals

@EnsuresNonNullIf(result=true,
                  expression="#1")
@Pure
public boolean equals(@GuardSatisfied Annotation this,
                      @GuardSatisfied @Nullable Object o)

Two annotations are equal iff their fields "daikonRep", "method" and "kind" are equal.

Overrides:

equals in class Object

hashCode

@Pure
public int hashCode(@GuardSatisfied Annotation this)

Overrides:

hashCode in class Object

get

public static Annotation get(Annotation.Kind kind,
                             String daikonRep,
                             String method,
                             String invRep,
                             String daikonClass)
                      throws Annotation.MalformedAnnotationException

Get the annotation with corresponding properties.

Throws:

Annotation.MalformedAnnotationException