cprover
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.