Go to the documentation of this file.
33 return std::make_shared<constant_index_ranget>(val);
69 const std::vector<abstract_object_pointert> &operands,
75 auto rounding_mode_symbol =
77 auto rounding_mode_value = environment.
eval(rounding_mode_symbol, ns);
78 auto rounding_mode_constant = rounding_mode_value->to_constant();
79 if(rounding_mode_constant.is_nil())
84 exprt adjusted_expr = expr;
86 exprt constant_replaced_expr = adjusted_expr;
87 constant_replaced_expr.
operands().clear();
94 const exprt &lhs_value = lhs_abstract_object->to_constant();
99 constant_replaced_expr.
operands().push_back(op);
105 constant_replaced_expr.
operands().push_back(lhs_value);
113 const exprt &lhs_value = lhs_abstract_object->to_constant();
117 simplified.
type(), ns,
true,
false);
133 auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
140 std::vector<abstract_object_pointert> possible_results;
141 for(
auto current_rounding_mode : rounding_modes)
145 rounding_mode_symbol,
149 mp_integer(
static_cast<unsigned long>(current_rounding_mode)),
155 std::vector<abstract_object_pointert> dummy;
156 possible_results.push_back(
159 auto first = possible_results.front()->to_constant();
160 for(
auto const &possible_result : possible_results)
162 auto current = possible_result->to_constant();
163 if(current.is_nil() || current != first)
168 return possible_results.front();
202 std::dynamic_pointer_cast<const constant_abstract_valuet>(other);
219 return std::make_shared<constant_abstract_valuet>(*other);
224 if(
value == other->value)
226 return shared_from_this();
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool is_top() const
Find out if the abstract object is top.
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
exprt to_constant() const override
Converts to a constant expression if possible.
index_range_ptrt make_constant_index_range(const exprt &val)
The type of an expression, extends irept.
abstract_object_pointert merge_constant_constant(const constant_abstract_value_pointert &other) const
Merges another constant abstract value into this one.
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
Base class for all expressions.
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Attempts to do a constant/constant merge if both are constants, otherwise falls back to the parent me...
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
Expression to hold a symbol (variable)
std::shared_ptr< index_ranget > index_range_ptrt
sharing_ptrt< constant_abstract_valuet > constant_abstract_value_pointert
Defines typet, type_with_subtypet and type_with_subtypest.
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.
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
index_range_ptrt make_indeterminate_index_range()
Fixed-width bit-vector with two's complement interpretation.
An abstract version of a program environment.
virtual exprt to_constant() const
Converts to a constant expression if possible.
exprt simplify_expr(exprt src, const namespacet &ns)
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
std::set< abstract_object_pointert > abstract_object_visitedt
constant_abstract_valuet(const typet &t)
index_range_ptrt index_range(const namespacet &ns) const override
constant_index_ranget(const exprt &val)
abstract_object_pointert try_transform_expr_with_all_rounding_modes(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) const
bool is_constant() const
Return whether the expression is a constant.
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
This is the basic interface of the abstract interpreter with default implementations of the core func...
std::size_t number_of_constants
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
virtual bool is_bottom() const
Find out if the abstract object is bottom.
API to expression classes.
static memory_sizet from_bytes(std::size_t bytes)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
An abstraction of a single value that just stores a constant.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.