cprover
contracts Directory Reference
+ Directory dependency graph for contracts:

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.