contracts Directory Reference

Directory dependency graph for contracts:

Directories
directory	doc
directory	dynamic-frames

Files
file	cfg_info.h [code]
	Classes providing CFG-based information about symbols to guide simplifications in function and loop assigns clause checking.
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	contracts_wrangler.cpp [code]
	Parse and annotate contracts.
file	contracts_wrangler.h [code]
	Parse and annotate contracts.
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	inlining_decorator.cpp [code]
file	inlining_decorator.h [code]
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	loop_contract_config.h [code]
	Config for loop contract.
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]