Go to the documentation of this file.
15 #include <unordered_set>
34 if(type.
id() == ID_struct_tag)
61 std::wstring out(length,
'?');
63 for(std::size_t i = 0; i < arr.
operands().size() && i < length; i++)
71 auto ref = std::ref(
static_cast<const exprt &
>(expr));
74 const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
75 const auto current_index =
77 entries[current_index] = with_expr.new_value();
78 ref = with_expr.old();
83 default_value = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
92 return std::accumulate(
98 const std::pair<std::size_t, exprt> &entry) {
99 const exprt entry_index = from_integer(entry.first, index.type());
100 const exprt &then_expr = entry.second;
101 CHECK_RETURN(then_expr.type() == if_expr.type());
102 const equal_exprt index_equal(index, entry_index);
103 return if_exprt(index_equal, then_expr, if_expr, if_expr.type());
109 return std::accumulate(
115 const std::pair<std::size_t, exprt> &entry) {
116 const exprt entry_index = from_integer(entry.first, index.type());
117 const exprt &then_expr = entry.second;
118 CHECK_RETURN(then_expr.type() == if_expr.type());
119 const binary_relation_exprt index_small_eq(index, ID_le, entry_index);
120 return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
126 const exprt &extra_value)
129 const auto &operands = expr.
operands();
130 exprt last_added = extra_value;
131 for(std::size_t i = 0; i < operands.size(); ++i)
133 const std::size_t index = operands.
size() - 1 - i;
134 if(operands[index].
id() != ID_unknown && operands[index] != last_added)
136 entries[index] = operands[index];
137 last_added = operands[index];
144 const exprt &extra_value)
148 for(std::size_t i = 0; i < expr.
operands().size(); i += 2)
150 const auto index = numeric_cast<std::size_t>(expr.
operands()[i]);
153 "all values in array should have the same type");
154 if(index.has_value() && expr.
operands()[i + 1].id() != ID_unknown)
162 if(
const auto &array_expr = expr_try_dynamic_cast<array_exprt>(expr))
164 if(
const auto &with_expr = expr_try_dynamic_cast<with_exprt>(expr))
166 if(
const auto &array_list = expr_try_dynamic_cast<array_list_exprt>(expr))
174 const auto it =
entries.lower_bound(index);
188 for(; it !=
entries.end() && it->first < size; ++it)
189 array.operands().resize(it->first + 1, it->second);
191 array.operands().resize(
Operator to update elements in structs and arrays.
const typet & subtype() const
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
std::size_t size() const
Amount of nodes this expression tree contains.
The type of an expression, extends irept.
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
Represents arrays by the indexes up to which the value remains the same.
exprt to_if_expression(const exprt &index) const
Base class for all expressions.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor,...
bitvector_typet index_type()
Magic numbers used throughout the codebase.
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
sparse_arrayt(const with_exprt &expr)
Initialize a sparse array from an expression of the form array_of(x) with {i:=a} with {j:=b} ....
static exprt to_if_expression(const with_exprt &expr, const exprt &index)
Creates an if_expr corresponding to the result of accessing the array at the given index.
interval_sparse_arrayt(const with_exprt &expr)
An expression of the form array_of(x) with {i:=a} with {j:=b} is converted to an array arr where for ...
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.
exprt at(std::size_t index) const
Get the value at the specified index.
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH
#define PRECONDITION(CONDITION)
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
static void utf16_native_endian_to_java_string(const wchar_t ch, std::ostringstream &result, const std::locale &loc)
Escapes non-printable characters, whitespace except for spaces, double quotes and backslashes.
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
nonstd::optional< T > optionalt
std::size_t get_width() const
Deprecated expression utility functions.
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
A Template Class for Graphs.
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
std::map< std::size_t, exprt > entries
Array constructor from a list of index-element pairs Operands are index/value pairs,...
API to expression classes.
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
Array constructor from list of elements.
bool can_cast_expr< with_exprt >(const exprt &base)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.