This class applies the loop contract transformation to a loop in a goto function. More...

#include <util/message.h>
#include <goto-programs/goto_model.h>
#include <analyses/local_may_alias.h>

Include dependency graph for dfcc_instrument_loop.h:

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

Classes
class	dfcc_instrument_loopt
	This class applies the loop contract transformation to a loop in a goto function. More...

Detailed Description

This class applies the loop contract transformation to a loop in a goto function.

Classes