CBMC
|
Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses of contracts. More...
Go to the source code of this file.
Classes | |
class | dfcc_is_freeablet |
Rewrites calls to is_freeable and was_freed predicates in goto programs encoding pre and post conditions. More... | |
Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses of contracts.
Definition in file dfcc_is_freeable.h.