Package daikon.tools.jtb

Class AnnotateVisitor

Object

DepthFirstVisitor

AnnotateVisitor

All Implemented Interfaces:

Visitor

public class AnnotateVisitor
extends DepthFirstVisitor

Field Summary

Fields

Modifier and Type	Field	Description
List<NodeToken>	addedComments
boolean	insert_inexpressible	If true, insert annotations not supported by ESC.
List<String>	javaFileLines
static String	JML_END_COMMENT
static String	JML_START_COMMENT
boolean	lightweight	If false, use full JML specs; if true, use lightweight ESC specs.
int	maxInvariantsPP	If the --max_invariants_pp option is given, this variable is set to the maximum number of invariants output by annotate per program point.
PptMap	ppts
boolean	slashslash	if true, use "//" comments; if false, use "/*" comments.
boolean	useReflection	Whether to use reflection when trying to figure out if a method overrides/implements another method.

Fields inherited from class DepthFirstVisitor

indent, indents

Constructor Summary

Constructors

Constructor	Description
AnnotateVisitor(String javafilename, Node root, PptMap ppts, boolean slashslash, boolean insert_inexpressible, boolean lightweight, boolean useReflection, int maxInvariantsPP)

Method Summary

Modifier and Type	Method	Description
String	format(Invariant inv)
static int	getTabbedIndex(int untabbedIndex, String L1)
void	insertAlso(Node n)
void	insertBehavior(Node n)
boolean	insertInvariants(Node n, String prefix, @Nullable AnnotateVisitor.InvariantsAndModifiedVars invs, boolean useJavaComment)
boolean	insertInvariants(Node n, String prefix, AnnotateVisitor.InvariantsAndModifiedVars invs)
void	insertJMLWorkaround(Node n)
boolean	insertModifies(Node n, String modifiesString, String prefix, boolean useJavaComment)
static AnnotateVisitor.InvariantsAndModifiedVars	invariants_for(PptTopLevel ppt, PptMap pptmap)
static String	precedingWhitespace(String s)	Return the whitespace at the front of the string.
boolean	pureInJML(Node n)
void	visit(ClassOrInterfaceDeclaration n)
void	visit(ConstructorDeclaration n)
void	visit(Expression n)
void	visit(FieldDeclaration n)
void	visit(MethodDeclaration n)
void	visit(StatementExpression n)

Methods inherited from class DepthFirstVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

JML_START_COMMENT

public static final String JML_START_COMMENT

JML_END_COMMENT

public static final String JML_END_COMMENT

javaFileLines

public List<String> javaFileLines

ppts

public PptMap ppts

slashslash

public boolean slashslash

if true, use "//" comments; if false, use "/*" comments.

insert_inexpressible

public boolean insert_inexpressible

If true, insert annotations not supported by ESC.

lightweight

public boolean lightweight

If false, use full JML specs; if true, use lightweight ESC specs.

useReflection

public boolean useReflection

Whether to use reflection when trying to figure out if a method overrides/implements another method. If this variable is set to false, then Annotate will not try to determine if a method overrides/implements another method, which means that it will not try to add "also" tags to its output.

maxInvariantsPP

public int maxInvariantsPP

If the --max_invariants_pp option is given, this variable is set to the maximum number of invariants output by annotate per program point.

addedComments

public List<NodeToken> addedComments

Constructor Detail

AnnotateVisitor

public AnnotateVisitor(String javafilename,
                       Node root,
                       PptMap ppts,
                       boolean slashslash,
                       boolean insert_inexpressible,
                       boolean lightweight,
                       boolean useReflection,
                       int maxInvariantsPP)

Method Detail

visit

public void visit(ClassOrInterfaceDeclaration n)

Specified by:

visit in interface Visitor

Overrides:

visit in class DepthFirstVisitor

visit

public void visit(FieldDeclaration n)

Specified by:

visit in interface Visitor

Overrides:

visit in class DepthFirstVisitor

insertAlso

public void insertAlso(Node n)

insertBehavior

public void insertBehavior(Node n)

visit

public void visit(MethodDeclaration n)

Specified by:

visit in interface Visitor

Overrides:

visit in class DepthFirstVisitor

visit

public void visit(ConstructorDeclaration n)

Specified by:

visit in interface Visitor

Overrides:

visit in class DepthFirstVisitor

pureInJML

public boolean pureInJML(Node n)

insertJMLWorkaround

public void insertJMLWorkaround(Node n)

insertInvariants

public boolean insertInvariants(Node n,
                                String prefix,
                                AnnotateVisitor.InvariantsAndModifiedVars invs)

insertModifies

public boolean insertModifies(Node n,
                              String modifiesString,
                              String prefix,
                              boolean useJavaComment)

insertInvariants

@EnsuresNonNullIf(result=true,
                  expression="#3")
public boolean insertInvariants(Node n,
                                String prefix,
                                @Nullable AnnotateVisitor.InvariantsAndModifiedVars invs,
                                boolean useJavaComment)

visit

public void visit(StatementExpression n)

Specified by:

visit in interface Visitor

Overrides:

visit in class DepthFirstVisitor

visit

public void visit(Expression n)

Specified by:

visit in interface Visitor

Overrides:

visit in class DepthFirstVisitor

format

public String format(Invariant inv)

invariants_for

public static AnnotateVisitor.InvariantsAndModifiedVars invariants_for(PptTopLevel ppt,
                                                                       PptMap pptmap)

getTabbedIndex

public static int getTabbedIndex(int untabbedIndex,
                                 String L1)

precedingWhitespace

public static String precedingWhitespace(String s)

Return the whitespace at the front of the string.