Local Typestate Checking

• The Typestate Checker works strictly intra-procedural (per method base). The goal is to avoid 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