Go to the documentation of this file.
23 const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr);
24 return symbol && !symbol->get_identifier().empty();
49 return *expr_try_dynamic_cast<symbol_exprt>(expr);
57 return symbol_operand.has_value();
97 if(
const auto sub_struct = expr_try_dynamic_cast<struct_exprt>(expr.
op0()))
106 [&](
const exprt &operand) { return operand.id() != ID_constant; }))
143 "Unsupported expression.");
145 if(
const auto member = expr_try_dynamic_cast<member_exprt>(lhs))
152 "Expecting a member with nested symbol operand.");
155 else if(
const auto symbol = expr_try_dynamic_cast<symbol_exprt>(lhs))
162 "Expecting a symbol with non-empty identifier.");
165 else if(
const auto index = expr_try_dynamic_cast<index_exprt>(lhs))
172 "Expecting an index expression with a symbol array and constant or "
173 "symbol index value.");
176 else if(
const auto byte = expr_try_dynamic_cast<byte_extract_exprt>(lhs))
183 "Expecting a byte extract expression with a symbol array and constant or "
184 "symbol index value.");
193 "Expression does not meet any trace assumptions.");
207 "Unsupported expression.");
209 if(
const auto address = expr_try_dynamic_cast<address_of_exprt>(rhs))
216 "Expecting an address of with nested symbol.");
219 else if(
const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(rhs))
226 "Expecting a symbol with non-empty identifier.");
229 else if(
const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(rhs))
236 "Expecting all non-base class operands to be constants.");
249 else if(
const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(rhs))
256 "Expecting the first operand of a constant expression to be a constant, "
257 "address_of or plus expression, or no operands and a non-empty value.");
260 else if(
const auto byte = expr_try_dynamic_cast<byte_extract_exprt>(rhs))
264 byte->operands().size() == 2,
267 "Expecting a byte extract with two operands.");
273 "Expecting a byte extract with constant value.");
279 "Expecting a byte extract with constant index.");
288 "Expression does not meet any trace assumptions.");
307 const bool run_check,
312 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)
bool can_cast_expr< address_of_exprt >(const exprt &base)
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< plus_exprt >(const exprt &base)
API to expression classes for Pointers.
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