Instruments occurrences of obeys_contract 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_obeys_contract.h:

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

Classes
class	dfcc_obeys_contractt
	Rewrites calls to obeys_contract predicates into calls to the library implementation. More...

Detailed Description

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

Classes