org.jmlspecs.jml4.compiler
Class JmlScannerAnnotationState

java.lang.Object
  org.jmlspecs.jml4.compiler.JmlScannerAnnotationState

public class JmlScannerAnnotationState
extends java.lang.Object

This is a helper class for the scanner. It helps manage which state the scanner is in relative to JML annotations and nested Java comments within JML annotations.

From the perspective of this class, the scanner is in one of the following states: (1) Not within a JML annotation. (2) Within a JML annotation but not within a nested Java comment. (3) Within a Java comment nested within a JML annotation. and (although this is beyond what is normally permitted by JML syntax) (4) Within a JML annotation nested within a JML annotation.

We allow (4) for now because it is a convenient means of supporting JML4-only syntax while allowing the overall source to remain JML2 compatible. E.g.

//@ public int array_of_int[/*#@non_null*\/];

Case 3 can take various forms such as:

//@ // Java comment within JML annotation. 
 //@ /* Java comment within JML annotation. *\/ 
 /*@ // Java comment within JML annotation.









Field Summary




static int
MAX_JML_ANNOTATION_NESTIN_LEVEL



           



static int
MULTI_LINE



           



static int
NOT_IN



           



static int
SINGLE_LINE



           


 



Constructor Summary
JmlScannerAnnotationState()



           
 



Method Summary




 boolean
canNestJmlAnnotation(boolean isSingleLineComment)



           



 boolean
endOfMultiLineComment()



           



 boolean
endOfSingleLineComment()



           



 int
jmlAnnotationNestingLevel()



           



 int
jmlAnnotationState()



           



 boolean
maxAnnotationNestingReached()



           



 int
nestedJavaCommentInJmlAnnotationState()



           



 boolean
processJml()



           



 void
resetJmlAnnotationState()



           



 void
resetNestedJavaCommentInJmlCommentState()



           



 void
startJmlAnnotation(boolean isSingleLine)



           



 void
startNestedJavaCommentInJmlAnnotation(boolean isSingleLine)



           



 java.lang.String
stateToString(int state)



           



 java.lang.String
toString()



           


 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
 





Field Detail



NOT_IN
public static final int NOT_IN


See Also:
Constant Field Values




SINGLE_LINE
public static final int SINGLE_LINE


See Also:
Constant Field Values




MULTI_LINE
public static final int MULTI_LINE


See Also:
Constant Field Values




MAX_JML_ANNOTATION_NESTIN_LEVEL
public static final int MAX_JML_ANNOTATION_NESTIN_LEVEL


See Also:
Constant Field Values





Constructor Detail



JmlScannerAnnotationState
public JmlScannerAnnotationState()






Method Detail



jmlAnnotationState
public int jmlAnnotationState()








processJml
public boolean processJml()



Returns:
true iff we are in a JML annotation but not within a nested Java comment.





nestedJavaCommentInJmlAnnotationState
public int nestedJavaCommentInJmlAnnotationState()








startJmlAnnotation
public void startJmlAnnotation(boolean isSingleLine)








resetJmlAnnotationState
public void resetJmlAnnotationState()








startNestedJavaCommentInJmlAnnotation
public void startNestedJavaCommentInJmlAnnotation(boolean isSingleLine)








resetNestedJavaCommentInJmlCommentState
public void resetNestedJavaCommentInJmlCommentState()








endOfSingleLineComment
public boolean endOfSingleLineComment()








endOfMultiLineComment
public boolean endOfMultiLineComment()








maxAnnotationNestingReached
public boolean maxAnnotationNestingReached()








jmlAnnotationNestingLevel
public int jmlAnnotationNestingLevel()








canNestJmlAnnotation
public boolean canNestJmlAnnotation(boolean isSingleLineComment)








toString
public java.lang.String toString()


Overrides:
toString in class java.lang.Object








stateToString
public java.lang.String stateToString(int state)