Instruments occurrences of pointer_in_range 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_pointer_in_range.h:

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

Classes
class	dfcc_pointer_in_ranget
	Rewrites calls to pointer_in_range predicates into calls to the library implementation. More...

Detailed Description

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

Classes