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