Typestate Checker Prototype

Contact:

If you have any comments whatsoever please write an email to This e-mail address is being protected from spambots. You need JavaScript enabled to view it . Thanks!

Features:

• (method-) local flow sensitive typestate checking for Java (still partial)
• (method-) local alias tracking (still partial)
• specify the typestate automaton with annotations
• keep in mind, this is a very early version!

Requirement:

• a JSR 308 compliant javac
• The Typestate Checker (link: October 2009 version)

How to use:

Simply run

javac -processor de.unisaarland.cs.st.jerify.verifier.Checker [your source files]

Make sure that you use the JSR 308 compiler and that the Typestate Checker's jar is in the class path (e.g. use -classpath /path/to/typestate.jar).

How to annotate:

read here ...