Features

The Jerify type-state verifier enables you to specify and enforce object usage protocols in Java.

Local Typestate Checking

• The Typestate Checker works strictly intra-procedural (per method base). The goal is to avoid the overhead of interprocedural analysis wherever possible. 
• Most Java language features that alter the flow are correctly checked
  
  • loops
      (including break / continue and labeled loops)
  • exceptions (only intraprodural)
  • switches
  • if / conditional expressoin
  • returns

Local Aliasing Tracking support

• Currently parameters and local variables are correctly tracked within each method
• method return values are treated as if they are newly created objects
  
  • working on typestate: objects should get the superset of typestate we analyzed for the called methods return values
  • working on alias: it should be checked if the returned values can be accessed from somewhere else (are aliased)
• direct field accesses are  unsupported
  
  • generally class.field accesses will not be allowed (checked) because they break encapsulation