cprover
Loading...
Searching...
No Matches
contracts Directory Reference
+ Directory dependency graph for contracts:

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