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
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
std::shared_ptr< index_ranget > index_range_ptrt
index_range_ptrt make_empty_index_range()
index_range_ptrt make_indeterminate_index_range()
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
virtual index_range_ptrt index_range(const namespacet &ns) const =0
abstract_value_objectt(const typet &type, bool tp, bool bttm)
abstract_value_objectt(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
abstract_value_objectt(const typet &type)
Base class for all expressions.
Definition: expr.h:54
virtual ~index_ranget()=default
virtual bool advance_to_next()=0
virtual const exprt & current() const =0
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
single_value_index_ranget(const exprt &val)
const exprt & current() const override
The type of an expression, extends irept.
Definition: type.h:28