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 
21 #include <util/std_expr.h>
22 
24 {
25 public:
26  explicit interval_abstract_valuet(const typet &t);
27  interval_abstract_valuet(const typet &t, bool tp, bool bttm);
28 
30 
32  const exprt &e,
33  const abstract_environmentt &environment,
34  const namespacet &ns);
35 
36  ~interval_abstract_valuet() override = default;
37 
39  index_range_implementation(const namespacet &ns) const override;
40 
42 
43  exprt to_constant() const override;
45  {
46  return interval;
47  }
48 
49  size_t internal_hash() const override;
50  bool internal_equality(const abstract_object_pointert &other) const override;
51 
52  void output(
53  std::ostream &out,
54  const class ai_baset &ai,
55  const class namespacet &ns) const override;
56 
57  void get_statistics(
58  abstract_object_statisticst &statistics,
59  abstract_object_visitedt &visited,
60  const abstract_environmentt &env,
61  const namespacet &ns) const override;
62 
63 protected:
64  CLONE
67  meet(const abstract_object_pointert &other) const override;
68 
69 private:
72 
77 
79 };
80 
81 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H
interval_abstract_valuet::index_range_implementation
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
Definition: interval_abstract_value.cpp:433
abstract_value_pointert
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
Definition: abstract_value_object.h:297
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
interval_abstract_valuet::output
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
Definition: interval_abstract_value.cpp:298
typet
The type of an expression, extends irept.
Definition: type.h:28
interval_abstract_valuet::~interval_abstract_valuet
~interval_abstract_valuet() override=default
interval_abstract_valuet
Definition: interval_abstract_value.h:24
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
sharing_ptrt
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
Definition: abstract_object.h:73
interval_abstract_valuet::merge_intervals
abstract_object_pointert merge_intervals(abstract_value_pointert &other) const
Merge another interval abstract object with this one.
Definition: interval_abstract_value.cpp:365
interval.h
CLONE
#define CLONE
Definition: abstract_object.h:47
interval_abstract_valuet::to_constant
exprt to_constant() const override
Converts to a constant expression if possible.
Definition: interval_abstract_value.cpp:264
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
value_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
Definition: abstract_value_object.h:130
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
interval_abstract_valuet::internal_hash
size_t internal_hash() const override
Definition: interval_abstract_value.cpp:285
interval_abstract_valuet::meet_intervals
abstract_object_pointert meet_intervals(interval_abstract_value_pointert other) const
Meet another interval abstract object with this one.
Definition: interval_abstract_value.cpp:406
interval_abstract_valuet::to_interval
constant_interval_exprt to_interval() const override
Definition: interval_abstract_value.h:44
interval_abstract_valuet::interval_abstract_value_pointert
sharing_ptrt< interval_abstract_valuet > interval_abstract_value_pointert
Definition: interval_abstract_value.h:71
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
abstract_value_objectt
Definition: abstract_value_object.h:240
interval_abstract_valuet::get_statistics
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
Definition: interval_abstract_value.cpp:449
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
interval_abstract_valuet::merge
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
Definition: interval_abstract_value.cpp:343
interval_abstract_valuet::internal_equality
bool internal_equality(const abstract_object_pointert &other) const override
Definition: interval_abstract_value.cpp:290
abstract_object_statistics.h
Statistics gathering for the variable senstivity domain.
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
interval_abstract_valuet::interval_abstract_valuet
interval_abstract_valuet(const typet &t)
Definition: interval_abstract_value.cpp:233
interval_abstract_valuet::meet
abstract_object_pointert meet(const abstract_object_pointert &other) const override
Base implementation of the meet operation: only used if no more precise abstraction can be used,...
Definition: interval_abstract_value.cpp:386
index_range_implementation_ptrt
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
Definition: abstract_value_object.h:25
interval_abstract_valuet::interval
constant_interval_exprt interval
Definition: interval_abstract_value.h:78
interval_abstract_valuet::value_range_implementation
value_range_implementation_ptrt value_range_implementation() const override
Definition: interval_abstract_value.cpp:444
std_expr.h
API to expression classes.
abstract_objectt::t
typet t
To enforce copy-on-write these are private and have read-only accessors.
Definition: abstract_object.h:361
abstract_value_object.h
Common behaviour for abstract objects modelling values - constants, intervals, etc.