22#define LOG(message, irep) \
25 log.debug().source_location = irep.source_location(); \
26 log.debug() << message << ": " << format(irep) << messaget::eom; \
38 :
log(message_handler), ns(ns), symbol_table(symbol_table)
53 const exprt &base_expression,
69 const exprt &expression)
const
167 LOG(
"Non const symbol wasn't squashed", simplified_expr);
181 LOG(
"Non-zero constant value found", simplified_expr);
187 LOG(
"Unrecognised expression", simplified_expr);
225 LOG(
"Could not resolve expression in array", value);
291 LOG(
"Struct was not const so can't resolve values on it",
member_expr);
343 LOG(
"Dereferenced value was not const so can't dereference",
deref_expr);
432 LOG(
"Non const symbol will not be squashed", simplified_expr);
586 "Squashing index of did not result in an array",
597 LOG(
"Failed to squash index of to array expression",
index_expr);
652 "Squashing member access did not resolve in a struct",
719 "Squashing dereference did not result in an address",
pointer_val);
778 const exprt &expression)
const
805 size_t component_number=
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A constant literal expression.
Operator to dereference a pointer.
Base class for all expressions.
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
bool get_bool(const irep_idt &name) const
const irep_idt & id() const
Extract member of struct or union.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
remove_const_function_pointerst(message_handlert &message_handler, const namespacet &ns, const symbol_table_baset &symbol_table)
To take a function call on a function pointer, and if possible resolve it to a small collection of po...
bool try_resolve_function_call(const exprt &expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
bool try_resolve_function_calls(const expressionst &exprs, functionst &out_functions)
To resolve a collection of expressions to the specific function calls they can be.
bool try_resolve_expression(const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
To squash various expr types to simplify the expression.
exprt get_component_value(const struct_exprt &struct_expr, const member_exprt &member_expr)
To extract the value of the specific component within a struct.
bool try_resolve_typecast(const typecast_exprt &typecast_expr, expressionst &out_expressions, bool &out_is_const)
To squash a typecast access.
bool try_resolve_dereference_function_call(const dereference_exprt &deref_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
bool try_resolve_member(const member_exprt &member_expr, expressionst &out_expressions, bool &out_is_const)
To squash an member access by first finding the struct it is accessing Then return the squashed value...
const symbol_table_baset & symbol_table
bool is_const_type(const typet &type) const
To evaluate the const-ness of the type.
bool try_resolve_index_of_function_call(const index_exprt &index_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
bool try_resolve_index_value(const exprt &index_value_expr, mp_integer &out_array_index)
Given an index into an array, resolve, if possible, the index that is being accessed.
bool operator()(const exprt &base_expression, functionst &out_functions)
To take a function call on a function pointer, and if possible resolve it to a small collection of po...
bool is_const_expression(const exprt &expression) const
To evaluate the const-ness of the expression type.
std::unordered_set< symbol_exprt, irep_hash > functionst
bool try_resolve_address_of_function_call(const address_of_exprt &address_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
bool try_resolve_member_function_call(const member_exprt &member_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
exprt resolve_symbol(const symbol_exprt &symbol_expr) const
Look up a symbol in the symbol table and return its value.
std::list< exprt > expressionst
bool try_resolve_index_of(const index_exprt &index_expr, expressionst &out_expressions, bool &out_is_const)
To squash an index access by first finding the array it is accessing Then if the index can be resolve...
bool try_resolve_dereference(const dereference_exprt &deref_expr, expressionst &out_expressions, bool &out_is_const)
To squash a dereference access by first finding the address_of the dereference is dereferencing.
bool try_resolve_typecast_function_call(const typecast_exprt &typecast_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
exprt replace_const_symbols(const exprt &expression) const
To collapse the symbols down to their values where possible This takes a very general approach,...
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The symbol table base class interface.
typet type
Type of symbol.
exprt value
Initial value of symbol.
Semantic type conversion.
The type of an expression, extends irept.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
#define LOG(message, irep)
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION(CONDITION)
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.