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