daikon.tools.jtb
Class AnnotateVisitor

Object
  DepthFirstVisitor
      AnnotateVisitor

All Implemented Interfaces:

Visitor

public class AnnotateVisitor
extends DepthFirstVisitor

Field Summary

Vector<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.

Constructor Summary

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

Method Summary

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, AnnotateVisitor.InvariantsAndModifiedVars invs)
boolean	insertInvariants(Node n, String prefix, AnnotateVisitor.InvariantsAndModifiedVars invs, boolean useJavaComment)
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) Grammar production: f0 -> ( "class" | "interface" ) f1 -> f2 -> [ TypeParameters() ] f3 -> [ ExtendsList(isInterface) ] f4 -> [ ImplementsList(isInterface) ] f5 -> ClassOrInterfaceBody(isInterface)
void	visit(ConstructorDeclaration n) Grammar production: f0 -> [ TypeParameters() ] f1 -> f2 -> FormalParameters() f3 -> [ "throws" NameList() ] f4 -> "{" f5 -> [ ExplicitConstructorInvocation() ] f6 -> ( BlockStatement() )* f7 -> "}"
void	visit(Expression n) f0 -> ConditionalExpression() f1 -> [ AssignmentOperator() Expression() ]
void	visit(FieldDeclaration n)
void	visit(MethodDeclaration n)
void	visit(StatementExpression n) f0 -> PreIncrementExpression() | PreDecrementExpression() | PrimaryExpression() [ "++" | "--" | AssignmentOperator() Expression() ]

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

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 Vector<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)

Grammar production: f0 -> ( "class" | "interface" ) f1 -> f2 -> [ TypeParameters() ] f3 -> [ ExtendsList(isInterface) ] f4 -> [ ImplementsList(isInterface) ] f5 -> ClassOrInterfaceBody(isInterface)

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)

Grammar production: f0 -> [ TypeParameters() ] f1 -> f2 -> FormalParameters() f3 -> [ "throws" NameList() ] f4 -> "{" f5 -> [ ExplicitConstructorInvocation() ] f6 -> ( BlockStatement() )* f7 -> "}"

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

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

visit

public void visit(StatementExpression n)

f0 -> PreIncrementExpression() | PreDecrementExpression() | PrimaryExpression() [ "++" | "--" | AssignmentOperator() Expression() ]

Specified by:

visit in interface Visitor

Overrides:

visit in class DepthFirstVisitor

visit

public void visit(Expression n)

f0 -> ConditionalExpression() f1 -> [ AssignmentOperator() Expression() ]

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.