![]() |
Download | Bugs | Reviews | Contact Us | Help |
Macros used to specify block invariants (this header is automatically included by contract.hpp).
CONTRACT_BLOCK_INVARIANT(assertions) CONTRACT_BLOCK_INVARIANT_TPL(assertions)
Macros used to program body definitions separately from the contract declarations (this header is automatically include by contract.hpp).
CONTRACT_FREE_BODY(function_name) CONTRACT_MEMBER_BODY(class_type, function_name) CONTRACT_CONSTRUCTOR_BODY(class_type, constructor_name) CONTRACT_DESTRUCTOR_BODY(class_type, destructor_name)
Contract broken handlers (this header is automatically included by contract.hpp).
namespace contract { class broken; enum from; typedef handler_function_pointer broken_contract_handler; // Set precondition broken handler to specified handler returning replaced handler. broken_contract_handler set_precondition_broken(broken_contract_handler handler); void precondition_broken(from const &); // Set postcondition broken handler to specified handler returning replaced handler. broken_contract_handler set_postcondition_broken(broken_contract_handler handler); void postcondition_broken(from const &); // Set handler for class invariant broken on entry to specified handler returning replaced handler. broken_contract_handler set_class_invariant_broken_on_entry(broken_contract_handler handler); void class_invariant_broken_on_entry(from const &); // Set handler for class invariant broken on exit to specified handler returning replaced handler. broken_contract_handler set_class_invariant_broken_on_exit(broken_contract_handler handler); void class_invariant_broken_on_exit(from const &); // Set handler for class invariant broken on throw to specified handler returning replaced handler. broken_contract_handler set_class_invariant_broken_on_throw(broken_contract_handler handler); void class_invariant_broken_on_throw(from const &); // For convenience, set all class invariant broken handlers (on entry, on exit, and on throw) to specified handler. void set_class_invariant_broken(broken_contract_handler handler); // Set block invariant broken handler to specified handler returning replaced handler. broken_contract_handler set_block_invariant_broken(broken_contract_handler handler); void block_invariant_broken(from const &); // Set the loop variant broken handler to specified handler returning replaced handler. broken_contract_handler set_loop_variant_broken(broken_contract_handler handler); void loop_variant_broken(from const &); }
Macros used to declare classes with contracts (this header is automatically included by contract.hpp).
CONTRACT_CLASS(class_declaration) CONTRACT_CLASS_TPL(class_declaration)
Macros used to specify class invariants (this header is automatically included by contract.hpp).
CONTRACT_CLASS_INVARIANT(class_invariants) CONTRACT_CLASS_INVARIANT_TPL(class_invariants)
Macros used to configure the library behaviour at compile-time (this header is automatically included by contract.hpp).
These configuration macros have appropriate default values if left undefined. Programmers can define these macros before including any of the library headers (using compiler options like -D for GCC, /D for MSVC, etc) in order to change the library behaviour.
The macros CONTRACT_CONFIG_NO_PRECONDITIONS, CONTRACT_CONFIG_NO_POSTCONDITIONS, etc can be defined to selectively disable compilation and run-time checking of all preconditions, postconditions, etc. This is a common practice in Contract Programming to generate debug and release builds with less correctness checks but faster run-times. Note that all contracts are compiled and checked at run-time by default unless specified otherwise using these configuration macros.
See also: Getting Started section, Contract Programming Overview section.
CONTRACT_CONFIG_NO_PRECONDITIONS CONTRACT_CONFIG_NO_POSTCONDITIONS CONTRACT_CONFIG_NO_CLASS_INVARIANTS CONTRACT_CONFIG_NO_BLOCK_INVARIANTS CONTRACT_CONFIG_NO_LOOP_VARIANTS CONTRACT_CONFIG_FUNCTION_ARITY_MAX CONTRACT_CONFIG_INHERITANCE_MAX CONTRACT_CONFIG_OLDOF_MAX CONTRACT_CONFIG_ARRAY_DIMENSION_MAX CONTRACT_CONFIG_DO_NOT_SUBCONTRACT_PRECONDITIONS CONTRACT_CONFIG_PRECONDITIONS_DISABLE_NO_ASSERTION CONTRACT_CONFIG_REPORT_BASE_PRECONDITION_FAILURE CONTRACT_CONFIG_THREAD_SAFE
Macros used to declare constructors with contracts (this header is automatically included by contract.hpp).
CONTRACT_CONSTRUCTOR(function_declaration) CONTRACT_CONSTRUCTOR_TPL(function_declaration)
Copy result value and old values for postconditions (this header is automatically included by contract.hpp).
namespace contract { template<typename T> class copy; }
Macros used to declare destructors with contracts (this header is automatically included by contract.hpp).
CONTRACT_DESTRUCTOR(function_declaration) CONTRACT_DESTRUCTOR_TPL(function_declaration)
Macros used to declare free functions, member functions, and operators with contracts (this header is automatically included by contract.hpp).
CONTRACT_FUNCTION(function_declaration) CONTRACT_FUNCTION_TPL(function_declaration)
Macros reporting bounds of some library constructs (this header is automatically included by contract.hpp).
These are not configuration macros so programmers cannot change these values. These macros are used to inform programmers of bounds on some of this library constructs.
CONTRACT_LIMIT_OLDOFS CONTRACT_LIMIT_NESTED_SELECT_ASSERTIONS CONTRACT_LIMIT_CONSTRUCTOR_TRY_BLOCK_CATCHES
Macros used to specify loop variants (this header is automatically included by contract.hpp).
CONTRACT_LOOP(loop_declaration) CONTRACT_LOOP_VARIANT(loop_variant) CONTRACT_LOOP_VARIANT_TPL(loop_variant)
Constructs to declare postcondition old values (this header is automatically included by contract.hpp).
CONTRACT_OLDOF
namespace contract { template<typename OldofExpressionType> struct has_oldof; }
Macros used to program named and deduced parameters (this header is automatically included by contract.hpp).
CONTRACT_CONSTRUCTOR_ARG(parameter_name) CONTRACT_PARAMETER_TYPEOF(parameter_name) CONTRACT_PARAMETER(named_parameter_declaration) CONTRACT_TEMPLATE_PARAMETER(named_parameter_declaration) CONTRACT_PARAMETER_BODY(function_name)