CBMC
|
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 | |