CBMC
Loading...
Searching...
No Matches
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