Package de.unisaarland.cs.st.jerify.verifier.quals

Provides for typestate Annotations which enable the user of this checker/analysis to annotate his/her code.

See:
          Description

Annotation Types Summary
ChangeState Annotate methods with this to signaling a change of the typestate of the receiver.
NoStateChanges This annotation will say that the method does not alter the typestate.
RecieverTypestate Asserts that the receiver of the method invocation can only be in the returnsTrueIsIn states if the method returns true, and only in the returnsFalseIsIn states if it returns false it has no effect on methods that do not return a boolean The effect on the typestate analysis is only that it is filtered with the possible states, the states are not added to the analysis.
RequireState Require that the typestate is in one of the states that is mention in isIn.
ReturnValue Asserts that the return Value of the method is in one of the state specified by isIn.
ScopeEndStates Classes that are annotated with this annotation are verified to be in the are States when the object has no references left pointing to it
SetState Set the typestate to the state mentioned in to.
TS Encapsulates several ChangeState Annotations, because multiple annotations are not allowed.
TypestateChecked Classes that are annotated with this annotation are forced to be typestate checked
 

Package de.unisaarland.cs.st.jerify.verifier.quals Description

Provides for typestate Annotations which enable the user of this checker/analysis to annotate his/her code.

Package Specification

none

Related Documentation

none