cprover
|
Files | |
contracts.cpp | |
Verify and use annotated loop and function contracts. | |
contracts.h | |
Verify and use annotated invariants and pre/post-conditions. | |
havoc_assigns_clause_targets.cpp | |
Havoc multiple and possibly dependent targets simultaneously. | |
havoc_assigns_clause_targets.h | |
Havoc function assigns clauses. | |
instrument_spec_assigns.cpp | |
Specify write set in code contracts. | |
instrument_spec_assigns.h | |
Specify write set in function contracts. | |
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 | |