cprover
interval_abstract_value.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity intervals
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H
14 
15 #include <iosfwd>
16 
17 #include <util/interval.h>
18 
20 
22 {
23 public:
24  explicit interval_abstract_valuet(const typet &t);
25  interval_abstract_valuet(const typet &t, bool tp, bool bttm);
26 
28  interval_abstract_valuet(const exprt &lower, const exprt &upper);
29 
31  const exprt &e,
32  const abstract_environmentt &environment,
33  const namespacet &ns);
34 
35  template <typename... Args>
36  static std::shared_ptr<interval_abstract_valuet>
37  make_interval(Args &&... args)
38  {
39  return std::make_shared<interval_abstract_valuet>(
40  std::forward<Args>(args)...);
41  }
42 
43  ~interval_abstract_valuet() override = default;
44 
46  index_range_implementation(const namespacet &ns) const override;
47 
49 
50  exprt to_constant() const override;
52  {
53  return interval;
54  }
55 
57  constrain(const exprt &lower, const exprt &upper) const override;
58 
59  size_t internal_hash() const override;
60  bool internal_equality(const abstract_object_pointert &other) const override;
61 
62  void output(
63  std::ostream &out,
64  const class ai_baset &ai,
65  const class namespacet &ns) const override;
66 
67  void get_statistics(
68  abstract_object_statisticst &statistics,
69  abstract_object_visitedt &visited,
70  const abstract_environmentt &env,
71  const namespacet &ns) const override;
72 
73 protected:
74  CLONE
75 
85  const abstract_value_pointert &other,
86  const widen_modet &widen_mode) const override;
87 
95  meet_with_value(const abstract_value_pointert &other) const override;
96 
97  exprt to_predicate_internal(const exprt &name) const override;
98 
99 private:
101 
102  void set_top_internal() override;
103 };
104 
105 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H
#define CLONE
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Common behaviour for abstract objects modelling values - constants, intervals, etc.
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
typet t
To enforce copy-on-write these are private and have read-only accessors.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
Represents an interval of values.
Definition: interval.h:48
Base class for all expressions.
Definition: expr.h:54
CLONE abstract_object_pointert merge_with_value(const abstract_value_pointert &other, const widen_modet &widen_mode) const override
Merge another interval abstract object with this one.
bool internal_equality(const abstract_object_pointert &other) const override
constant_interval_exprt to_interval() const override
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_value_pointert constrain(const exprt &lower, const exprt &upper) const override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override
Meet another interval abstract object with this one.
value_range_implementation_ptrt value_range_implementation() const override
size_t internal_hash() const override
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
~interval_abstract_valuet() override=default
constant_interval_exprt interval
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The type of an expression, extends irept.
Definition: type.h:29