contracts Directory Reference

Directory dependency graph for contracts:

Directories
	doc
	dynamic-frames

Files
	cfg_info.h
	Classes providing CFG-based information about symbols to guide simplifications in function and loop assigns clause checking.
	contracts.cpp
	Verify and use annotated loop and function contracts.
	contracts.h
	Verify and use annotated invariants and pre/post-conditions.
	contracts_wrangler.cpp
	Parse and annotate contracts.
	contracts_wrangler.h
	Parse and annotate contracts.
	havoc_assigns_clause_targets.cpp
	Havoc multiple and possibly dependent targets simultaneously.
	havoc_assigns_clause_targets.h
	Havoc function assigns clauses.
	inlining_decorator.cpp
	inlining_decorator.h
	instrument_spec_assigns.cpp
	Specify write set in code contracts.
	instrument_spec_assigns.h
	Specify write set in function contracts.
	loop_contract_config.h
	Config for loop contract.
	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