Code Contracts User Documentation

CBMC supports Function Contracts and Loop Contracts.

The individual types of clauses for contracts are documented here:

• Requires and Ensures Clauses
• Assigns Clauses
• Frees Clauses
• Loop Invariant Clauses
• Decreases Clauses
• Memory Predicates
• Function Pointer Predicates
• History Variables
• Quantifiers
• Command Line Interface for Code Contracts