[−] List of all items
Macros
- assume
- assume_preconditions
- assume_unreachable
- assumed_postcondition
- checked_assume
- checked_assume_eq
- checked_assume_ne
- checked_postcondition
- checked_postcondition_eq
- checked_postcondition_ne
- checked_precondition
- checked_precondition_eq
- checked_precondition_ne
- checked_verify
- checked_verify_eq
- checked_verify_ne
- debug_checked_assume
- debug_checked_assume_eq
- debug_checked_assume_ne
- debug_checked_postcondition
- debug_checked_postcondition_eq
- debug_checked_postcondition_ne
- debug_checked_precondition
- debug_checked_precondition_eq
- debug_checked_precondition_ne
- debug_checked_verify
- debug_checked_verify_eq
- debug_checked_verify_ne
- get_model_field
- postcondition
- precondition
- result
- set_model_field
- verify
- verify_unreachable