contracts Directory Reference

Directory dependency graph for contracts:

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