CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
10
11#include <util/interval.h>
12#include <util/string_utils.h>
13
14#include <algorithm>
15
16static bool by_length(const std::string &lhs, const std::string &rhs)
17{
18 if(lhs.size() < rhs.size())
19 return true;
20 if(lhs.size() > rhs.size())
21 return false;
22 return lhs < rhs;
23}
24
26 std::ostream &out,
27 const ai_baset &ai,
28 const namespacet &ns) const
29{
30 std::vector<std::string> output_values;
31 for(const auto &value : values)
32 {
33 std::ostringstream ss;
34 value->output(ss, ai, ns);
35 output_values.emplace_back(ss.str());
36 }
37 std::sort(output_values.begin(), output_values.end(), by_length);
38
39 join_strings(out, output_values.begin(), output_values.end(), ", ");
40}
41
43{
44 PRECONDITION(!values.empty());
45
46 auto initial =
47 std::dynamic_pointer_cast<const abstract_value_objectt>(first())
48 ->to_interval();
49
50 if(initial.is_boolean() && values.size() == 2) // must be both true and false
52
53 exprt lower_expr = initial.get_lower();
54 exprt upper_expr = initial.get_upper();
55
56 for(const auto &value : values)
57 {
58 const auto &v =
59 std::dynamic_pointer_cast<const abstract_value_objectt>(value);
60 const auto &value_expr = v->to_interval();
65 }
67}
static bool by_length(const std::string &lhs, const std::string &rhs)
an unordered set of value objects
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
abstract_object_pointert first() const
constant_interval_exprt to_interval() const
Calculate the set of values as an interval.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Represents an interval of values.
Definition interval.h:52
static exprt get_max(const exprt &a, const exprt &b)
Definition interval.cpp:960
static exprt get_min(const exprt &a, const exprt &b)
Definition interval.cpp:965
Base class for all expressions.
Definition expr.h:56
The Boolean constant false.
Definition std_expr.h:3199
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The Boolean constant true.
Definition std_expr.h:3190
#define PRECONDITION(CONDITION)
Definition invariant.h:463
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.