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;
154 if(range_start==-1 ||
to_integer(simp_offset, index))
164 be.
id()==ID_byte_extract_little_endian,
166 assert(index<std::numeric_limits<size_t>::max());
168 range_start + map.map_bit(numeric_cast_v<std::size_t>(index));
185 const auto dist = numeric_cast<mp_integer>(simp_distance);
186 if(range_start == -1 || size == -1 || src_size == -1 || !dist.has_value())
199 if(shift.
id()==ID_ashr || shift.
id()==ID_lshr)
202 sh_range_start+=dist_r;
204 range_spect sh_size=std::min(size, src_size-sh_range_start);
206 if(sh_range_start>=0 && sh_range_start<src_size)
211 assert(src_size-dist_r>=0);
212 range_spect sh_size=std::min(size, src_size-dist_r);
227 if(type.
id()==ID_union ||
241 if(offset_bits.has_value())
244 offset += range_start;
258 if(expr.
array().
id() == ID_null_object)
264 if(type.
id()==ID_vector)
270 sub_size = subtype_bits.has_value() ?
to_range_spect(*subtype_bits) : -1;
272 else if(type.
id()==ID_array)
278 sub_size = subtype_bits.has_value() ?
to_range_spect(*subtype_bits) : -1;
285 const auto index = numeric_cast<mp_integer>(simp_index);
286 if(!index.has_value())
289 if(range_start == -1 || sub_size == -1 || !index.has_value())
312 if(subtype_bits.has_value())
323 range_spect full_r_s=range_start==-1 ? 0 : range_start;
325 size==-1 ? sub_size*expr.
operands().size() : full_r_s+size;
329 if(full_r_s<=offset+sub_size && full_r_e>offset)
331 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
333 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
357 range_spect full_r_s=range_start==-1 ? 0 : range_start;
358 range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
370 else if(sub_size==-1)
372 if(full_r_e==-1 || full_r_e>offset)
374 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
381 else if(full_r_e==-1)
383 if(full_r_s<=offset+sub_size)
385 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
392 else if(full_r_s<=offset+sub_size && full_r_e>offset)
394 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
396 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
419 else if(new_size!=-1)
421 if(new_size<=range_start)
424 new_size-=range_start;
425 new_size=std::min(size, new_size);
433 if(
object.
id() == ID_string_constant ||
434 object.
id() == ID_label ||
435 object.
id() == ID_array ||
436 object.
id() == ID_null_object)
439 else if(
object.
id()==ID_symbol)
441 else if(
object.
id()==ID_dereference)
443 else if(
object.
id()==ID_index)
450 else if(
object.
id()==ID_member)
456 else if(
object.
id()==ID_if)
464 else if(
object.
id()==ID_byte_extract_little_endian ||
465 object.
id()==ID_byte_extract_big_endian)
471 else if(
object.
id()==ID_typecast)
478 throw "rw_range_sett: address_of `"+
object.id_string()+
"' not handled";
487 objectst::iterator entry=
490 std::pair<
const irep_idt &, std::unique_ptr<range_domain_baset>>(
491 identifier,
nullptr))
494 if(entry->second==
nullptr)
495 entry->second=util_make_unique<range_domaint>();
497 static_cast<range_domaint&>(*entry->second).push_back(
498 {range_start, range_end});
507 if(expr.
id() == ID_complex_real)
510 else if(expr.
id() == ID_complex_imag)
513 else if(expr.
id()==ID_typecast)
519 else if(expr.
id()==ID_if)
521 else if(expr.
id()==ID_dereference)
527 else if(expr.
id()==ID_byte_extract_little_endian ||
528 expr.
id()==ID_byte_extract_big_endian)
534 else if(expr.
id()==ID_shl ||
535 expr.
id()==ID_ashr ||
538 else if(expr.
id()==ID_member)
540 else if(expr.
id()==ID_index)
542 else if(expr.
id()==ID_array)
544 else if(expr.
id()==ID_struct)
546 else if(expr.
id()==ID_symbol)
557 (full_size>0 && range_start>=full_size))
563 else if(range_start>=0)
565 range_spect range_end=size==-1 ? -1 : range_start+size;
566 if(size!=-1 && full_size!=-1)
567 range_end=std::min(range_end, full_size);
569 add(mode, identifier, range_start, range_end);
572 add(mode, identifier, 0, -1);
584 else if(expr.
id() == ID_null_object ||
585 expr.
id() == ID_string_constant)
595 throw "rw_range_sett: assignment to `"+expr.
id_string()+
"' not handled";
610 if(type.
id()==ID_array)
637 if(type_bits.has_value())
641 if(range_start == -1 || new_size <= range_start)
645 new_size -= range_start;
646 new_size = std::min(size, new_size);
654 if(
object.is_not_nil() && !
has_subexpr(
object, ID_dereference))
659 const namespacet &ns, std::ostream &out)
const
668 out << itr->first <<
":" << itr->second.first;
671 out <<
" if " <<
from_expr(ns,
"", itr->second.second);
708 objectst::iterator entry=
711 std::pair<
const irep_idt &, std::unique_ptr<range_domain_baset>>(
712 identifier,
nullptr))
715 if(entry->second==
nullptr)
716 entry->second=util_make_unique<guarded_range_domaint>();
718 static_cast<guarded_range_domaint&>(*entry->second).insert(
738 function_call.
lhs());
782 if(target->code.get(ID_statement)==ID_printf)
837 goto_functionst::function_mapt::const_iterator f_it=
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
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)
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.
void add(const exprt &expr)
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.
Base class for all expressions.
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
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)
exprt simplify_expr(const exprt &src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
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.
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
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.
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.
virtual void get_objects_rec(goto_programt::const_targett, get_modet mode, const exprt &expr)
Expression classes for byte-level operators.
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
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)
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
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)
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)
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
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
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
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.
A generic container class for the GOTO intermediate representation of one function.
exprt dereference(const exprt &pointer, const namespacet &ns)
Dereference the given pointer-expression.
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)
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
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.
#define CHECK_RETURN(CONDITION)