14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
72 std::vector<assigns_clause_targett *>
targets;
Operator to return the address of an object.
A base class for assigns clause targets.
assigns_clause_targett(const exprt &object, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
exprt alias_expression(const exprt &lhs)
const exprt & get_direct_pointer() const
~assigns_clause_targett()
std::vector< symbol_exprt > temporary_declarations() const
const exprt pointer_object
exprt compatible_expression(const assigns_clause_targett &called_target)
const irep_idt & target_id
goto_programt & get_init_block()
const code_contractst & contract
static exprt pointer_for(const exprt &object)
goto_programt havoc_code()
exprt alias_expression(const exprt &lhs)
goto_programt init_block()
const irep_idt function_id
assigns_clause_targett * add_target(exprt target)
goto_programt standin_declarations
exprt compatible_expression(const assigns_clauset &called_assigns)
std::vector< assigns_clause_targett * > targets
goto_programt dead_stmts()
assigns_clauset(const exprt &assigns, code_contractst &contract, const irep_idt function_id, messaget log_parameter)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A generic container class for the GOTO intermediate representation of one function.
Class that provides messages with a built-in verbosity 'level'.
Expression to hold a symbol (variable)
Verify and use annotated invariants and pre/post-conditions.