CBMC
|
Instruments occurrences of obeys_contract predicates in programs encoding requires and ensures clauses of contracts. More...
Go to the source code of this file.
Classes | |
class | dfcc_obeys_contractt |
Rewrites calls to obeys_contract predicates into calls to the library implementation. More... | |
Instruments occurrences of obeys_contract predicates in programs encoding requires and ensures clauses of contracts.
Definition in file dfcc_obeys_contract.h.