Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses of contracts. More...

#include <util/message.h>
#include <goto-programs/goto_program.h>

Include dependency graph for dfcc_is_freeable.h:

This graph shows which files directly or indirectly include 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...

Detailed Description

Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses of contracts.

Definition in file dfcc_is_freeable.h.

Classes