Skip to content

Commit 8329afd

Browse files
committed
Enable cross-representation expression transform for all values
Implement abstract_value_objectt::expression_transform, and prevent further overriding. Within that, dispatch according to the types of the operands - * any are value sets, iterate over all of the combinations and dispatch for each of these, producing a value set to contain all of the results * mixed constant and interval, convert all constants to intervals and handle as all intervals * all interval, do interval arithmetic * all constant, substitute and simplify
1 parent 3a1428f commit 8329afd

10 files changed

+624
-497
lines changed

src/analyses/variable-sensitivity/abstract_object_set.cpp

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@
77
\*******************************************************************/
88

99
#include <analyses/variable-sensitivity/abstract_object_set.h>
10+
#include <analyses/variable-sensitivity/interval_abstract_value.h>
11+
#include <util/interval.h>
1012
#include <util/string_utils.h>
1113

1214
static bool by_length(const std::string &lhs, const std::string &rhs)
@@ -34,3 +36,19 @@ void abstract_object_sett::output(
3436

3537
join_strings(out, output_values.begin(), output_values.end(), ", ");
3638
}
39+
40+
abstract_object_pointert abstract_object_sett::to_interval()
41+
{
42+
PRECONDITION(!values.empty());
43+
44+
exprt lower_expr = first()->to_constant();
45+
exprt upper_expr = first()->to_constant();
46+
for(const auto &value : values)
47+
{
48+
const auto &value_expr = value->to_constant();
49+
lower_expr = constant_interval_exprt::get_min(lower_expr, value_expr);
50+
upper_expr = constant_interval_exprt::get_max(upper_expr, value_expr);
51+
}
52+
return std::make_shared<interval_abstract_valuet>(
53+
constant_interval_exprt(lower_expr, upper_expr));
54+
}

src/analyses/variable-sensitivity/abstract_object_set.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,11 @@ class abstract_object_sett
8080
void
8181
output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const;
8282

83+
/// Cast the set of values \p other_values to an interval.
84+
/// \param other_values: the value-set to be abstracted into an interval
85+
/// \return the interval-abstract-object containing \p other_values
86+
abstract_object_pointert to_interval();
87+
8388
private:
8489
value_sett values;
8590
};

0 commit comments

Comments
 (0)