14 const exprt &expression,
26 const auto find_result = type_size_map.find(
pointer_type->base_type());
27 if(find_result != type_size_map.cend())
29 exprt pointer_size_expr;
43 pointer_size_expr = pointer_size_opt.value();
51 type_size_map.emplace_hint(
52 find_result,
pointer_type->base_type(), pointer_size_term);
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
Base class for all expressions.
void visit_pre(std::function< void(exprt &)>)
typet & type()
Return the type of the expression.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
std::unordered_map< exprt, decision_procedure_objectt, irep_hash > smt_object_mapt
Mapping from an object's base expression to the set of information about it which we track.
API to expression classes for Pointers.
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt object_size(const exprt &pointer)
#define PRECONDITION(CONDITION)
smt_function_application_termt::factoryt< smt_command_functiont > make_applicationt
Function which makes applications of the smt function.
smt_function_application_termt::factoryt< smt_command_functiont > make_applicationt
Function which makes applications of the smt function.
void associate_pointer_sizes(const exprt &expression, const namespacet &ns, type_size_mapt &type_size_map, const smt_object_mapt &object_map, const smt_object_sizet::make_applicationt &object_size, const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
This function populates the (pointer) type -> size map.
Utilities for making a map of types to associated sizes.
std::unordered_map< typet, smt_termt, irep_hash > type_size_mapt