Annotations

This chapter defines the syntax and the semantics of the various contructs that may appear inside VeriFast annotations.

• Keywords
• Types
• Expressions
• Assertions
• Function specifications
• Function body annotations
  • Ghost commands
  • Block annotations
  • Call annotations
• Ghost declarations