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