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);
92 assert(op.
type().
id()==ID_complex);
98 (range_start==-1 || expr.
id()==ID_complex_real) ? 0 : sub_size;
143 if(range_start==-1 ||
to_integer(simp_offset, index))
153 be.
id()==ID_byte_extract_little_endian,
155 assert(index<std::numeric_limits<size_t>::max());
173 if(range_start==-1 ||
189 if(shift.
id()==ID_ashr || shift.
id()==ID_lshr)
192 sh_range_start+=dist_r;
194 range_spect sh_size=std::min(size, src_size-sh_range_start);
196 if(sh_range_start>=0 && sh_range_start<src_size)
201 assert(src_size-dist_r>=0);
202 range_spect sh_size=std::min(size, src_size-dist_r);
217 if(type.
id()==ID_union ||
245 if(expr.
array().
id() == ID_null_object)
251 if(type.
id()==ID_vector)
258 else if(type.
id()==ID_array)
277 if(range_start==-1 ||
310 range_spect full_r_s=range_start==-1 ? 0 : range_start;
312 size==-1 ? sub_size*expr.
operands().size() : full_r_s+size;
316 if(full_r_s<=offset+sub_size && full_r_e>offset)
318 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
320 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
342 range_spect full_r_s=range_start==-1 ? 0 : range_start;
343 range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
354 else if(sub_size==-1)
356 if(full_r_e==-1 || full_r_e>offset)
358 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
365 else if(full_r_e==-1)
367 if(full_r_s<=offset+sub_size)
369 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
376 else if(full_r_s<=offset+sub_size && full_r_e>offset)
378 range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
380 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
402 else if(new_size!=-1)
404 if(new_size<=range_start)
407 new_size-=range_start;
408 new_size=std::min(size, new_size);
416 if(
object.
id() == ID_string_constant ||
417 object.
id() == ID_label ||
418 object.
id() == ID_array ||
419 object.
id() == ID_null_object)
422 else if(
object.
id()==ID_symbol)
424 else if(
object.
id()==ID_dereference)
426 else if(
object.
id()==ID_index)
433 else if(
object.
id()==ID_member)
439 else if(
object.
id()==ID_if)
447 else if(
object.
id()==ID_byte_extract_little_endian ||
448 object.
id()==ID_byte_extract_big_endian)
454 else if(
object.
id()==ID_typecast)
461 throw "rw_range_sett: address_of `"+
object.id_string()+
"' not handled";
470 objectst::iterator entry=
473 std::pair<
const irep_idt &, std::unique_ptr<range_domain_baset>>(
474 identifier,
nullptr))
477 if(entry->second==
nullptr)
478 entry->second=util_make_unique<range_domaint>();
481 {range_start, range_end});
490 if(expr.
id()==ID_complex_real ||
491 expr.
id()==ID_complex_imag)
493 else if(expr.
id()==ID_typecast)
499 else if(expr.
id()==ID_if)
501 else if(expr.
id()==ID_dereference)
507 else if(expr.
id()==ID_byte_extract_little_endian ||
508 expr.
id()==ID_byte_extract_big_endian)
514 else if(expr.
id()==ID_shl ||
515 expr.
id()==ID_ashr ||
518 else if(expr.
id()==ID_member)
520 else if(expr.
id()==ID_index)
522 else if(expr.
id()==ID_array)
524 else if(expr.
id()==ID_struct)
526 else if(expr.
id()==ID_symbol)
534 (full_size>0 && range_start>=full_size))
540 else if(range_start>=0)
542 range_spect range_end=size==-1 ? -1 : range_start+size;
543 if(size!=-1 && full_size!=-1)
544 range_end=std::min(range_end, full_size);
546 add(mode, identifier, range_start, range_end);
549 add(mode, identifier, 0, -1);
561 else if(expr.
id() == ID_null_object ||
562 expr.
id() == ID_string_constant)
572 throw "rw_range_sett: assignment to `"+expr.
id_string()+
"' not handled";
585 if(type.
id()==ID_array)
610 if(range_start==-1 || new_size<=range_start)
614 new_size-=range_start;
615 new_size=std::min(size, new_size);
620 if(
object.is_not_nil() && !
has_subexpr(
object, ID_dereference))
625 const namespacet &ns, std::ostream &out)
const 634 out << itr->first <<
":" << itr->second.first;
637 out <<
" if " <<
from_expr(ns,
"", itr->second.second);
674 objectst::iterator entry=
677 std::pair<
const irep_idt &, std::unique_ptr<range_domain_baset>>(
678 identifier,
nullptr))
681 if(entry->second==
nullptr)
682 entry->second=util_make_unique<guarded_range_domaint>();
704 function_call.
lhs());
748 if(target->code.get(ID_statement)==ID_printf)
803 goto_functionst::function_mapt::const_iterator f_it=
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
goto_programt::const_targett target
const exprt & return_value() const
const code_declt & to_code_decl(const codet &code)
sub_typet::const_iterator const_iterator
Maps a big-endian offset to a little-endian offset.
#define forall_rw_range_set_w_objects(it, rw_set)
exprt simplify_expr(const exprt &src, const namespacet &ns)
const code_deadt & to_code_dead(const codet &code)
sub_typet::const_iterator const_iterator
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
Deprecated expression utility functions.
const irep_idt & get_identifier() const
#define forall_expr(it, expr)
Goto Programs with Functions.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
range_spect to_range_spect(const mp_integer &size)
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_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)
function_mapt function_map
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)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Extract member of struct or union.
void output(const namespacet &ns, std::ostream &out) const override
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
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)
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
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)
instructionst::const_iterator const_targett
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 member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const code_returnt & to_code_return(const codet &code)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
virtual void get_objects_rec(goto_programt::const_targett, get_modet mode, const exprt &expr)
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
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
A generic container class for the GOTO intermediate representation of one function.
#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)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
const exprt & struct_op() const
irep_idt get_component_name() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
virtual void output(const namespacet &ns, std::ostream &out) const override
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
const std::string & id_string() const
goto_programt & goto_program
Expression to hold a symbol (variable)
virtual ~range_domain_baset()
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
mp_integer member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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 index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
A base class for shift operators.
void output(std::ostream &out) const
array constructor from list of elements
void add(const exprt &expr)
const code_function_callt & to_code_function_call(const codet &code)