cprover
abstract_value_object.h
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 
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_VALUE_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_VALUE_OBJECT_H
14 
16 
18 {
19 };
20 
22 {
23 public:
24  virtual ~index_ranget() = default;
25  virtual const exprt &current() const = 0;
26  virtual bool advance_to_next() = 0;
27 };
28 
30 {
31 protected:
32  explicit single_value_index_ranget(const exprt &val);
33 
34 public:
35  const exprt &current() const override;
36  bool advance_to_next() override;
37 
38 private:
39  const exprt value;
40  bool available;
41 };
42 
43 typedef std::shared_ptr<index_ranget> index_range_ptrt;
44 
47 
49  public abstract_value_tag
50 {
51 public:
53  {
54  }
55 
56  abstract_value_objectt(const typet &type, bool tp, bool bttm)
57  : abstract_objectt(type, tp, bttm)
58  {
59  }
60 
62  const exprt &expr,
63  const abstract_environmentt &environment,
64  const namespacet &ns)
65  : abstract_objectt(expr, environment, ns)
66  {
67  }
68 
69  virtual index_range_ptrt index_range(const namespacet &ns) const = 0;
70 };
71 
72 #endif
index_ranget
Definition: abstract_value_object.h:22
single_value_index_ranget
Definition: abstract_value_object.h:30
typet
The type of an expression, extends irept.
Definition: type.h:28
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:53
single_value_index_ranget::current
const exprt & current() const override
Definition: abstract_value_object.cpp:40
abstract_value_objectt::index_range
virtual index_range_ptrt index_range(const namespacet &ns) const =0
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
single_value_index_ranget::value
const exprt value
Definition: abstract_value_object.h:39
make_empty_index_range
index_range_ptrt make_empty_index_range()
Definition: abstract_value_object.cpp:52
index_range_ptrt
std::shared_ptr< index_ranget > index_range_ptrt
Definition: abstract_value_object.h:43
abstract_object.h
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
index_ranget::advance_to_next
virtual bool advance_to_next()=0
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
abstract_value_objectt::abstract_value_objectt
abstract_value_objectt(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Definition: abstract_value_object.h:61
single_value_index_ranget::single_value_index_ranget
single_value_index_ranget(const exprt &val)
Definition: abstract_value_object.cpp:35
abstract_value_tag
Definition: abstract_value_object.h:18
abstract_value_objectt
Definition: abstract_value_object.h:50
index_ranget::current
virtual const exprt & current() const =0
abstract_value_objectt::abstract_value_objectt
abstract_value_objectt(const typet &type, bool tp, bool bttm)
Definition: abstract_value_object.h:56
make_indeterminate_index_range
index_range_ptrt make_indeterminate_index_range()
Definition: abstract_value_object.cpp:57
index_ranget::~index_ranget
virtual ~index_ranget()=default
single_value_index_ranget::available
bool available
Definition: abstract_value_object.h:40
single_value_index_ranget::advance_to_next
bool advance_to_next() override
Definition: abstract_value_object.cpp:45
abstract_objectt
Definition: abstract_object.h:79
abstract_value_objectt::abstract_value_objectt
abstract_value_objectt(const typet &type)
Definition: abstract_value_object.h:52