cprover
abstract_object_set.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Jez Higgins, jez@jezuk.co.uk
6 
7 \*******************************************************************/
8 
11 #include <util/interval.h>
12 #include <util/string_utils.h>
13 
14 static bool by_length(const std::string &lhs, const std::string &rhs)
15 {
16  if(lhs.size() < rhs.size())
17  return true;
18  if(lhs.size() > rhs.size())
19  return false;
20  return lhs < rhs;
21 }
22 
24  std::ostream &out,
25  const ai_baset &ai,
26  const namespacet &ns) const
27 {
28  std::vector<std::string> output_values;
29  for(const auto &value : values)
30  {
31  std::ostringstream ss;
32  value->output(ss, ai, ns);
33  output_values.emplace_back(ss.str());
34  }
35  std::sort(output_values.begin(), output_values.end(), by_length);
36 
37  join_strings(out, output_values.begin(), output_values.end(), ", ");
38 }
39 
41 {
42  PRECONDITION(!values.empty());
43 
44  const auto &initial =
45  std::dynamic_pointer_cast<const abstract_value_objectt>(first());
46 
47  exprt lower_expr = initial->to_interval().get_lower();
48  exprt upper_expr = initial->to_interval().get_upper();
49  for(const auto &value : values)
50  {
51  const auto &v =
52  std::dynamic_pointer_cast<const abstract_value_objectt>(value);
53  const auto &value_expr = v->to_interval();
54  lower_expr =
55  constant_interval_exprt::get_min(lower_expr, value_expr.get_lower());
56  upper_expr =
57  constant_interval_exprt::get_max(upper_expr, value_expr.get_upper());
58  }
59  return constant_interval_exprt(lower_expr, upper_expr);
60 }
string_utils.h
constant_interval_exprt::get_max
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:959
exprt
Base class for all expressions.
Definition: expr.h:54
interval.h
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
by_length
static bool by_length(const std::string &lhs, const std::string &rhs)
Definition: abstract_object_set.cpp:14
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
abstract_object_set.h
an unordered set of value objects
join_strings
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:62
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
abstract_object_sett::first
abstract_object_pointert first() const
Definition: abstract_object_set.h:47
interval_abstract_value.h
An interval to represent a set of possible values.
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
abstract_object_sett::values
value_sett values
Definition: abstract_object_set.h:88
abstract_object_sett::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
Definition: abstract_object_set.cpp:23
constant_interval_exprt::get_min
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:964
abstract_object_sett::to_interval
constant_interval_exprt to_interval() const
Calculate the set of values as an interval.
Definition: abstract_object_set.cpp:40