36 for(const_iterator itr=begin();
42 out << itr->first <<
":" << itr->second;
49 for(rw_range_sett::objectst::iterator it=r_range_set.begin();
50 it!=r_range_set.end();
54 for(rw_range_sett::objectst::iterator it=w_range_set.begin();
55 it!=w_range_set.end();
65 out <<
" " << it->first;
66 it->second->output(ns, out);
75 out <<
" " << it->first;
76 it->second->output(ns, out);
88 assert(op.
type().
id()==ID_complex);
94 (range_start==-1 || expr.
id()==ID_complex_real) ? 0 : sub_size;
139 if(range_start==-1 ||
to_integer(simp_offset, index))
149 be.
id()==ID_byte_extract_little_endian,
151 assert(index<std::numeric_limits<size_t>::max());
169 if(range_start==-1 ||
185 if(shift.
id()==ID_ashr || shift.
id()==ID_lshr)
188 sh_range_start+=dist_r;
190 range_spect sh_size=std::min(size, src_size-sh_range_start);
192 if(sh_range_start>=0 && sh_range_start<src_size)
197 assert(src_size-dist_r>=0);
198 range_spect sh_size=std::min(size, src_size-dist_r);
213 if(type.
id()==ID_union ||
241 if(expr.
array().
id()==
"NULL-object")
247 if(type.
id()==ID_vector)
271 if(range_start==-1 ||
304 range_spect full_r_s=range_start==-1 ? 0 : range_start;
306 size==-1 ? sub_size*expr.
operands().size() : full_r_s+size;
310 if(full_r_s<=offset+sub_size && full_r_e>offset)
312 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
314 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
336 range_spect full_r_s=range_start==-1 ? 0 : range_start;
337 range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
348 else if(sub_size==-1)
350 if(full_r_e==-1 || full_r_e>offset)
352 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
359 else if(full_r_e==-1)
361 if(full_r_s<=offset+sub_size)
363 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
370 else if(full_r_s<=offset+sub_size && full_r_e>offset)
372 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
374 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
396 else if(new_size!=-1)
398 if(new_size<=range_start)
401 new_size-=range_start;
402 new_size=std::min(size, new_size);
410 if(
object.
id()==ID_string_constant ||
411 object.
id()==ID_label ||
412 object.
id()==ID_array ||
413 object.
id()==
"NULL-object")
416 else if(
object.
id()==ID_symbol)
418 else if(
object.
id()==ID_dereference)
420 else if(
object.
id()==ID_index)
427 else if(
object.
id()==ID_member)
433 else if(
object.
id()==ID_if)
441 else if(
object.
id()==ID_byte_extract_little_endian ||
442 object.
id()==ID_byte_extract_big_endian)
448 else if(
object.
id()==ID_typecast)
455 throw "rw_range_sett: address_of `"+
object.id_string()+
"' not handled";
464 objectst::iterator entry=(mode==
get_modet::LHS_W ? w_range_set : r_range_set).
466 std::pair<const irep_idt&, range_domain_baset*>(
467 identifier,
nullptr)).first;
469 if(entry->second==
nullptr)
473 std::make_pair(range_start, range_end));
482 if(expr.
id()==ID_complex_real ||
483 expr.
id()==ID_complex_imag)
484 get_objects_complex(mode, expr, range_start, size);
485 else if(expr.
id()==ID_typecast)
486 get_objects_typecast(
491 else if(expr.
id()==ID_if)
492 get_objects_if(mode,
to_if_expr(expr), range_start, size);
493 else if(expr.
id()==ID_dereference)
494 get_objects_dereference(
499 else if(expr.
id()==ID_byte_extract_little_endian ||
500 expr.
id()==ID_byte_extract_big_endian)
501 get_objects_byte_extract(
506 else if(expr.
id()==ID_shl ||
507 expr.
id()==ID_ashr ||
509 get_objects_shift(mode,
to_shift_expr(expr), range_start, size);
510 else if(expr.
id()==ID_member)
511 get_objects_member(mode,
to_member_expr(expr), range_start, size);
512 else if(expr.
id()==ID_index)
513 get_objects_index(mode,
to_index_expr(expr), range_start, size);
514 else if(expr.
id()==ID_array)
515 get_objects_array(mode,
to_array_expr(expr), range_start, size);
516 else if(expr.
id()==ID_struct)
517 get_objects_struct(mode,
to_struct_expr(expr), range_start, size);
518 else if(expr.
id()==ID_symbol)
526 (full_size>0 && range_start>=full_size))
532 else if(range_start>=0)
534 range_spect range_end=size==-1 ? -1 : range_start+size;
535 if(size!=-1 && full_size!=-1)
536 range_end=std::max(range_end, full_size);
538 add(mode, identifier, range_start, range_end);
541 add(mode, identifier, 0, -1);
553 else if(expr.
id()==
"NULL-object" ||
554 expr.
id()==ID_string_constant)
564 throw "rw_range_sett: assignment to `"+expr.
id_string()+
"' not handled";
577 if(type.
id()==ID_array)
602 if(range_start==-1 || new_size<=range_start)
606 new_size-=range_start;
607 new_size=std::min(size, new_size);
612 if(
object.is_not_nil() &&
618 const namespacet &ns, std::ostream &out)
const 621 for(const_iterator itr=begin();
627 out << itr->first <<
":" << itr->second.first;
628 out <<
" if " <<
from_expr(ns,
"", itr->second.second);
647 guardt guard_bak1(guard), guard_bak2(guard);
651 guard.swap(guard_bak1);
653 guard.add(if_expr.
cond());
655 guard.swap(guard_bak2);
665 objectst::iterator entry=(mode==
get_modet::LHS_W ? w_range_set : r_range_set).
667 std::pair<const irep_idt&, range_domain_baset*>(
668 identifier,
nullptr)).first;
670 if(entry->second==
nullptr)
674 std::make_pair(range_start,
675 std::make_pair(range_end, guard.as_expr())));
694 function_call.
lhs());
737 if(target->code.get(ID_statement)==ID_printf)
792 goto_functionst::function_mapt::const_iterator f_it=
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
The type of an expression.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const exprt & return_value() const
const code_declt & to_code_decl(const codet &code)
Maps a big-endian offset to a little-endian offset.
#define forall_rw_range_set_w_objects(it, rw_set)
virtual void output(const namespacet &ns, std::ostream &out) const
exprt simplify_expr(const exprt &src, const namespacet &ns)
const code_deadt & to_code_dead(const codet &code)
const irep_idt & get_identifier() const
#define forall_expr(it, expr)
Goto Programs with Functions.
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
range_spect to_range_spect(const mp_integer &size)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
virtual void get_objects_member(get_modet mode, const member_exprt &expr, const range_spect &range_start, const range_spect &size)
The trinary if-then-else operator.
virtual void get_objects_index(get_modet mode, const index_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual void get_objects_complex(get_modet mode, const exprt &expr, const range_spect &range_start, const range_spect &size)
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
Extract member of struct or union.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
instructionst::const_iterator const_targett
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
void get_objects_rec(get_modet mode, const exprt &expr, object_id_sett &dest, const std::string &suffix)
Expression classes for byte-level operators.
exprt dereference(const exprt &pointer, const namespacet &ns)
virtual void get_objects_address_of(const exprt &object)
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Operator to dereference a pointer.
A constant-size array type.
API to expression classes.
virtual void get_objects_byte_extract(get_modet mode, const byte_extract_exprt &be, 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)
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
const code_returnt & to_code_return(const codet &code)
#define forall_operands(it, expr)
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
virtual void get_objects_shift(get_modet mode, const shift_exprt &shift, const range_spect &range_start, const range_spect &size)
Operator to return the address of an object.
function_mapt function_map
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
virtual void get_objects_array(get_modet mode, const array_exprt &expr, const range_spect &range_start, const range_spect &size)
bool has_return_value() const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
virtual void output(const namespacet &ns, std::ostream &out) const
#define forall_rw_range_set_r_objects(it, rw_set)
virtual void get_objects_typecast(get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size)
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
Base class for all expressions.
const exprt & struct_op() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
static bool has_dereference(const exprt &expr)
Returns 'true' iff the given expression contains unary '*'.
irep_idt get_component_name() const
const std::string & id_string() const
Expression to hold a symbol (variable)
virtual ~range_domain_baset()
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
struct constructor from list of elements
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
#define forall_goto_program_instructions(it, program)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
A base class for shift operators.
void output(std::ostream &out) const
array constructor from list of elements
const code_function_callt & to_code_function_call(const codet &code)