Instruments occurrences of is_fresh 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_fresh.h:

This graph shows which files directly or indirectly include this file:

Classes
class	dfcc_is_fresht
	Rewrites calls to is_fresh predicates into calls to the library implementation. More...

Detailed Description

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

Definition in file dfcc_is_fresh.h.

Classes