cprover
|
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"
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... | |
Specify write set in function contracts.
Definition in file instrument_spec_assigns.h.