32 target_id(object.id())
36 "Assigns clause targets should be stored as pointer expressions.");
43 function_symbol.
mode);
59 std::vector<symbol_exprt> result;
93 target_offset.
type()),
120 const exprt &assigns,
126 function_id(function_id),
146 (target.
id() == ID_address_of)
162 target->get_init_block().instructions)
175 for(
symbol_exprt symbol : target->temporary_declarations())
181 return dead_statements;
192 return havoc_statements;
206 condition.push_back(target->alias_expression(lhs));
214 if(called_assigns.
targets.empty())
219 bool first_clause =
true;
223 bool first_iter =
true;
241 current_target_compatible =
or_exprt(
244 target->compatible_expression(*called_target));
248 current_target_compatible =
249 target->compatible_expression(*called_target);
255 current_target_compatible =
or_exprt(
256 current_target_compatible,
257 target->compatible_expression(*called_target));
262 result = current_target_compatible;
263 first_clause =
false;
268 conjuncts.push_back(result);
269 conjuncts.push_back(current_target_compatible);
Specify write set in function contracts.
unsignedbv_typet unsigned_int_type()
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)
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)
A base class for relations, i.e., binary predicates whose two operands have the same type.
A codet representing an assignment in the program.
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &mode)
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
The Boolean constant false.
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The plus expression Associativity is not specified.
Expression to hold a symbol (variable)
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
irep_idt mode
Language mode.
The Boolean constant true.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
A predicate that indicates that an address range is ok to write.
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
Utilities for building havoc code for expressions.
std::set< exprt > modifiest
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.