Go to the documentation of this file.
46 out << itr->first <<
":" << itr->second;
53 for(rw_range_sett::objectst::iterator it=
r_range_set.begin();
58 for(rw_range_sett::objectst::iterator it=
w_range_set.begin();
69 out <<
" " << it->first;
70 it->second->output(
ns, out);
79 out <<
" " << it->first;
80 it->second->output(
ns, out);
109 (range_start==-1 || expr.
id()==ID_complex_real) ? 0 : sub_size;
153 auto index = numeric_cast<mp_integer>(simp_offset);
154 if(range_start == -1 || !index.has_value())
164 be.
id()==ID_byte_extract_little_endian,
167 range_start + map.
map_bit(numeric_cast_v<std::size_t>(*index));
184 const auto dist = numeric_cast<mp_integer>(simp_distance);
185 if(range_start == -1 || size == -1 || src_size == -1 || !dist.has_value())
198 if(shift.
id()==ID_ashr || shift.
id()==ID_lshr)
201 sh_range_start+=dist_r;
203 range_spect sh_size=std::min(size, src_size-sh_range_start);
205 if(sh_range_start>=0 && sh_range_start<src_size)
210 assert(src_size-dist_r>=0);
211 range_spect sh_size=std::min(size, src_size-dist_r);
226 if(type.
id() == ID_union || type.
id() == ID_union_tag || range_start == -1)
239 if(offset_bits.has_value())
242 offset += range_start;
256 if(expr.
array().
id() == ID_null_object)
262 if(type.
id()==ID_vector)
268 sub_size = subtype_bits.has_value() ?
to_range_spect(*subtype_bits) : -1;
270 else if(type.
id()==ID_array)
276 sub_size = subtype_bits.has_value() ?
to_range_spect(*subtype_bits) : -1;
283 const auto index = numeric_cast<mp_integer>(simp_index);
284 if(!index.has_value())
287 if(range_start == -1 || sub_size == -1 || !index.has_value())
309 if(subtype_bits.has_value())
320 range_spect full_r_s=range_start==-1 ? 0 : range_start;
322 size==-1 ? sub_size*expr.
operands().size() : full_r_s+size;
326 if(full_r_s<=offset+sub_size && full_r_e>offset)
328 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
330 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
354 range_spect full_r_s=range_start==-1 ? 0 : range_start;
355 range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
367 else if(sub_size==-1)
369 if(full_r_e==-1 || full_r_e>offset)
371 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
378 else if(full_r_e==-1)
380 if(full_r_s<=offset+sub_size)
382 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
389 else if(full_r_s<=offset+sub_size && full_r_e>offset)
391 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
393 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
416 else if(new_size!=-1)
418 if(new_size<=range_start)
421 new_size-=range_start;
422 new_size=std::min(size, new_size);
430 if(
object.
id() == ID_string_constant ||
431 object.
id() == ID_label ||
432 object.
id() == ID_array ||
433 object.
id() == ID_null_object)
438 else if(
object.
id()==ID_symbol)
442 else if(
object.
id()==ID_dereference)
446 else if(
object.
id()==ID_index)
453 else if(
object.
id()==ID_member)
459 else if(
object.
id()==ID_if)
467 else if(
object.
id()==ID_byte_extract_little_endian ||
468 object.
id()==ID_byte_extract_big_endian)
474 else if(
object.
id()==ID_typecast)
481 throw "rw_range_sett: address_of '" +
object.id_string() +
"' not handled";
490 objectst::iterator entry=
493 std::pair<
const irep_idt &, std::unique_ptr<range_domain_baset>>(
494 identifier,
nullptr))
497 if(entry->second==
nullptr)
498 entry->second=util_make_unique<range_domaint>();
501 {range_start, range_end});
510 if(expr.
id() == ID_complex_real)
513 else if(expr.
id() == ID_complex_imag)
516 else if(expr.
id()==ID_typecast)
522 else if(expr.
id()==ID_if)
524 else if(expr.
id()==ID_dereference)
530 else if(expr.
id()==ID_byte_extract_little_endian ||
531 expr.
id()==ID_byte_extract_big_endian)
537 else if(expr.
id()==ID_shl ||
538 expr.
id()==ID_ashr ||
541 else if(expr.
id()==ID_member)
543 else if(expr.
id()==ID_index)
545 else if(expr.
id()==ID_array)
547 else if(expr.
id()==ID_struct)
549 else if(expr.
id()==ID_symbol)
560 (full_size>0 && range_start>=full_size))
566 else if(range_start>=0)
568 range_spect range_end=size==-1 ? -1 : range_start+size;
569 if(size!=-1 && full_size!=-1)
570 range_end=std::min(range_end, full_size);
572 add(mode, identifier, range_start, range_end);
575 add(mode, identifier, 0, -1);
587 else if(expr.
id() == ID_null_object ||
588 expr.
id() == ID_string_constant)
598 throw "rw_range_sett: assignment to '" + expr.
id_string() +
"' not handled";
613 if(type.
id()==ID_array)
640 if(type_bits.has_value())
644 if(range_start == -1 || new_size <= range_start)
648 new_size -= range_start;
649 new_size = std::min(size, new_size);
657 if(
object.is_not_nil() && !
has_subexpr(
object, ID_dereference))
662 const namespacet &ns, std::ostream &out)
const
671 out << itr->first <<
":" << itr->second.first;
701 guard = std::move(copy);
711 objectst::iterator entry=
714 std::pair<
const irep_idt &, std::unique_ptr<range_domain_baset>>(
715 identifier,
nullptr))
718 if(entry->second==
nullptr)
719 entry->second=util_make_unique<guarded_range_domaint>();
774 target->get_condition());
792 if(target->get_other().get_statement() == ID_printf)
794 for(
const auto &op : target->get_other().operands())
846 goto_rw(
function, i_it, rw_set);
853 goto_functionst::function_mapt::const_iterator f_it=
860 goto_rw(f_it->first, body, rw_set);
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
const typet & subtype() const
virtual void get_objects_shift(get_modet mode, const shift_exprt &shift, const range_spect &range_start, const range_spect &size)
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
sub_typet::const_iterator const_iterator
#define forall_rw_range_set_r_objects(it, rw_set)
virtual void get_objects_address_of(const exprt &object)
virtual void get_objects_array(get_modet mode, const array_exprt &expr, const range_spect &range_start, const range_spect &size)
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_declt & to_code_decl(const codet &code)
virtual void get_objects_byte_extract(get_modet mode, const byte_extract_exprt &be, const range_spect &range_start, const range_spect &size)
#define CHECK_RETURN(CONDITION)
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
The type of an expression, extends irept.
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Operator to dereference a pointer.
virtual void get_objects_typecast(get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size)
The trinary if-then-else operator.
Real part of the expression describing a complex number.
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
function_mapt function_map
void output(const namespacet &ns, std::ostream &out) const override
Expression to hold a symbol (variable)
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
virtual void get_objects_member(get_modet mode, const member_exprt &expr, const range_spect &range_start, const range_spect &size)
range_spect to_range_spect(const mp_integer &size)
bool is_false() const
Return whether the expression is a constant representing false.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Struct constructor from list of elements.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
codet representation of a function call statement.
const array_typet & type() const
Expression classes for byte-level operators.
void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size) override
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define forall_operands(it, expr)
const exprt & struct_op() const
void add(const exprt &expr)
const code_deadt & to_code_dead(const codet &code)
const irep_idt & get_identifier() const
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
size_t map_bit(size_t bit) const
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
const std::string & id_string() const
virtual void get_objects_complex_imag(get_modet mode, const complex_imag_exprt &expr, const range_spect &range_start, const range_spect &size)
exprt simplify_expr(exprt src, const namespacet &ns)
virtual void get_objects_index(get_modet mode, const index_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual ~range_domain_baset()
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
goto_programt::const_targett target
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
const code_returnt & to_code_return(const codet &code)
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
void output(std::ostream &out) const
#define forall_rw_range_set_w_objects(it, rw_set)
Extract member of struct or union.
Deprecated expression utility functions.
A collection of goto functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
A base class for shift operators.
bool has_return_value() const
Structure type, corresponds to C style structs.
codet representation of a "return from a function" statement.
const code_assignt & to_code_assign(const codet &code)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Imaginary part of the expression describing a complex number.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Maps a big-endian offset to a little-endian offset.
Goto Programs with Functions.
A generic container class for the GOTO intermediate representation of one function.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
virtual void get_objects_complex_real(get_modet mode, const complex_real_exprt &expr, const range_spect &range_start, const range_spect &size)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
instructionst::const_iterator const_targett
irep_idt get_component_name() const
virtual void output(const namespacet &ns, std::ostream &out) const override
#define forall_expr(it, expr)
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
Operator to return the address of an object.
Semantic type conversion.
const exprt & return_value() const
A codet representing an assignment in the program.
sub_typet::const_iterator const_iterator
void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size) override
API to expression classes.
Array constructor from list of elements.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
#define forall_goto_program_instructions(it, program)
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.