instrument_spec_assigns.h File Reference

Specify write set in function contracts. More...

#include <optional>
#include <unordered_map>
#include <unordered_set>
#include <ansi-c/c_expr.h>
#include <goto-programs/goto_program.h>
#include <util/message.h>
#include "utils.h"

Include dependency graph for instrument_spec_assigns.h:

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

Go to the source code of this file.

Classes
class	conditional_target_exprt
	Class that represents a single conditional target. More...
class	car_exprt
	Class that represents a normalized conditional address range, with: More...
class	instrument_spec_assignst
	A class that generates instrumentation for assigns clause checking. More...

Detailed Description

Specify write set in function contracts.

Definition in file instrument_spec_assigns.h.