contracts Directory Reference

Directory dependency graph for contracts:

Files
file	contracts.cpp [code]
	Verify and use annotated loop and function contracts.
file	contracts.h [code]
	Verify and use annotated invariants and pre/post-conditions.
file	havoc_assigns_clause_targets.cpp [code]
	Havoc multiple and possibly dependent targets simultaneously.
file	havoc_assigns_clause_targets.h [code]
	Havoc function assigns clauses.
file	instrument_spec_assigns.cpp [code]
	Specify write set in code contracts.
file	instrument_spec_assigns.h [code]
	Specify write set in function contracts.
file	memory_predicates.cpp [code]
	Predicates to specify memory footprint in function contracts.
file	memory_predicates.h [code]
	Predicates to specify memory footprint in function contracts.
file	utils.cpp [code]
file	utils.h [code]