cprover
|
Files | |
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 | 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 | instrument_spec_assigns.cpp [code] |
Specify write set in code contracts. | |
file | instrument_spec_assigns.h [code] |
Specify write set in function contracts. | |
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] |