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