daikon.tools.jtb
Object
Annotation
public class Annotation extends Object
Utility class to parse annotations generated with the Annotate program
using --wrap_xml flag.
An example of the String representation of an annotation, as output
with the --wrap_xml flag, is:
this.topOfStack <= this.theArray.length-1
this.topOfStack <= size(this.theArray[])-1
class daikon.inv.binary.twoScalar.IntLessEqual
isEmpty()
The above string should actually span only one line.
To be well-formed, an annotation should be enclosed in
tags, contain
and
tags,
and exactly one of
,
,
, or
.
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.
daikonClass
public String daikonClass
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 annoString may contain
none, one, or several annotations. Malformed annotations are
ignored.
daikonRep
public String daikonRep
The way this annotation would be printed by Daikon.
method
public String method
The method that this annotation refers to.
kind
public Annotation.Kind kind
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.
toString
public String toString
Easy-on-the-eye format.
Overrides: toString Object
equals
public boolean equals Object o)
Two annotations are equal iff their fields "daikonRep", "method"
and "kind" are equal.
Overrides: equals Object
hashCode
public int hashCode
Overrides: hashCode Object
get
public static Annotation get Annotation.Kind kind,
String daikonRep,
String method)
throws Annotation.MalformedAnnotationException
Get the annotation with corresponding properties.
Throws:
Annotation.MalformedAnnotationException
Annotation