Go to the documentation of this file.
22 const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr);
23 return symbol && !symbol->get_identifier().empty();
48 return *expr_try_dynamic_cast<symbol_exprt>(expr);
56 return symbol_operand.has_value();
96 if(
const auto sub_struct = expr_try_dynamic_cast<struct_exprt>(expr.
op0()))
105 [&](
const exprt &operand) { return operand.id() != ID_constant; }))
142 "Unsupported expression.");
144 if(
const auto member = expr_try_dynamic_cast<member_exprt>(lhs))
151 "Expecting a member with nested symbol operand.");
154 else if(
const auto symbol = expr_try_dynamic_cast<symbol_exprt>(lhs))
161 "Expecting a symbol with non-empty identifier.");
164 else if(
const auto index = expr_try_dynamic_cast<index_exprt>(lhs))
171 "Expecting an index expression with a symbol array and constant or "
172 "symbol index value.");
175 else if(
const auto byte = expr_try_dynamic_cast<byte_extract_exprt>(lhs))
182 "Expecting a byte extract expression with a symbol array and constant or "
183 "symbol index value.");
192 "Expression does not meet any trace assumptions.");
206 "Unsupported expression.");
208 if(
const auto address = expr_try_dynamic_cast<address_of_exprt>(rhs))
215 "Expecting an address of with nested symbol.");
218 else if(
const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(rhs))
225 "Expecting a symbol with non-empty identifier.");
228 else if(
const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(rhs))
235 "Expecting all non-base class operands to be constants.");
248 else if(
const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(rhs))
255 "Expecting the first operand of a constant expression to be a constant, "
256 "address_of or plus expression, or no operands and a non-empty value.");
259 else if(
const auto byte = expr_try_dynamic_cast<byte_extract_exprt>(rhs))
263 byte->operands().size() == 2,
266 "Expecting a byte extract with two operands.");
272 "Expecting a byte extract with constant value.");
278 "Expecting a byte extract with constant index.");
287 "Expression does not meet any trace assumptions.");
306 const bool run_check,
311 for(
const auto &step : trace.
steps)
Class that provides messages with a built-in verbosity 'level'.
bool can_cast_expr< symbol_exprt >(const exprt &base)
void check_trace_assumptions(const goto_tracet &trace, const namespacet &ns, const messaget &log, const bool run_check, const validation_modet vm)
Checks that the structure of each step of the trace matches certain criteria.
bool can_cast_expr< array_list_exprt >(const exprt &base)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
optionalt< symbol_exprt > get_inner_symbol_expr(exprt expr)
Recursively extracts the first operand of an expression until it reaches a symbol and returns it,...
static void check_step_assumptions(const goto_trace_stept &step, const namespacet &ns, const validation_modet vm)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
mstreamt & status() const
bool check_struct_structure(const struct_exprt &expr)
bool valid_lhs_expr_high_level(const exprt &lhs)
bool check_symbol_structure(const exprt &expr)
Base class for all expressions.
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
Step of the trace of a GOTO program.
bool can_cast_expr< byte_extract_exprt >(const exprt &base)
bool can_cast_expr< array_exprt >(const exprt &base)
bool can_cast_expr< member_exprt >(const exprt &base)
static void check_lhs_assumptions(const exprt &lhs, const namespacet &ns, const validation_modet vm)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
bool is_assignment() const
Struct constructor from list of elements.
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.
Expression classes for byte-level operators.
bool check_index_structure(const exprt &index_expr)
bool can_evaluate_to_constant(const exprt &expression)
bool has_operands() const
Return true if there is at least one operand.
bool can_cast_expr< address_of_exprt >(const exprt &base)
bool can_cast_expr< plus_exprt >(const exprt &base)
bool check_member_structure(const member_exprt &expr)
exprt simplify_expr(exprt src, const namespacet &ns)
static void check_rhs_assumptions(const exprt &rhs, const namespacet &ns, const validation_modet vm)
nonstd::optional< T > optionalt
bool check_address_structure(const address_of_exprt &address)
bool can_cast_expr< index_exprt >(const exprt &base)
Extract member of struct or union.
Deprecated expression utility functions.
bool valid_rhs_expr_high_level(const exprt &rhs)
static bool may_be_lvalue(const exprt &expr)
bool can_cast_expr< typecast_exprt >(const exprt &base)
bool check_constant_structure(const constant_exprt &constant_expr)
bool can_cast_expr< constant_exprt >(const exprt &base)
Operator to return the address of an object.
A constant literal expression.
bool can_cast_expr< struct_exprt >(const exprt &base)
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
API to expression classes.
const irep_idt & get_value() const