cprover
constant_abstract_value.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_ABSTRACT_VALUE_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_ABSTRACT_VALUE_H
14 
15 #include <iosfwd>
16 
18 #include <util/std_expr.h>
19 
21 {
22 public:
23  explicit constant_abstract_valuet(const typet &t);
24  explicit constant_abstract_valuet(const exprt &t);
25  constant_abstract_valuet(const typet &t, bool tp, bool bttm);
27  const exprt &e,
28  const abstract_environmentt &environment,
29  const namespacet &ns);
30 
31  ~constant_abstract_valuet() override = default;
32 
34  index_range_implementation(const namespacet &ns) const override;
35 
37 
38  exprt to_constant() const override;
39  constant_interval_exprt to_interval() const override;
40 
41  void output(
42  std::ostream &out,
43  const class ai_baset &ai,
44  const class namespacet &ns) const override;
45 
46  void get_statistics(
47  abstract_object_statisticst &statistics,
48  abstract_object_visitedt &visited,
49  const abstract_environmentt &env,
50  const namespacet &ns) const override;
51 
52  size_t internal_hash() const override
53  {
54  return std::hash<std::string>{}(value.pretty());
55  }
56 
57  bool internal_equality(const abstract_object_pointert &other) const override
58  {
59  auto cast_other =
60  std::dynamic_pointer_cast<const constant_abstract_valuet>(other);
61  return cast_other && value == cast_other->value;
62  }
63 
64 protected:
65  CLONE
66 
74 
75 private:
85 
87 };
88 
89 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_ABSTRACT_VALUE_H
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
constant_abstract_valuet::to_constant
exprt to_constant() const override
Converts to a constant expression if possible.
Definition: constant_abstract_value.cpp:82
constant_abstract_valuet::internal_equality
bool internal_equality(const abstract_object_pointert &other) const override
Definition: constant_abstract_value.h:57
typet
The type of an expression, extends irept.
Definition: type.h:28
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:501
constant_abstract_valuet::internal_hash
size_t internal_hash() const override
Definition: constant_abstract_value.h:52
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
constant_abstract_valuet::merge
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Attempts to do a constant/constant merge if both are constants, otherwise falls back to the parent me...
Definition: constant_abstract_value.cpp:115
CLONE
#define CLONE
Definition: abstract_object.h:47
constant_abstract_valuet::value
exprt value
Definition: constant_abstract_value.h:86
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
constant_abstract_valuet::~constant_abstract_valuet
~constant_abstract_valuet() override=default
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
constant_abstract_valuet::merge_constant_constant
abstract_object_pointert merge_constant_constant(const abstract_value_pointert &other) const
Merges another abstract value into this one.
Definition: constant_abstract_value.cpp:125
constant_abstract_valuet::value_range_implementation
value_range_implementation_ptrt value_range_implementation() const override
Definition: constant_abstract_value.cpp:77
constant_abstract_valuet::output
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
Definition: constant_abstract_value.cpp:99
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
abstract_value_objectt
Definition: abstract_value_object.h:240
constant_abstract_valuet
Definition: constant_abstract_value.h:21
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
constant_abstract_valuet::constant_abstract_valuet
constant_abstract_valuet(const typet &t)
Definition: constant_abstract_value.cpp:40
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
constant_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: constant_abstract_value.cpp:138
index_range_implementation_ptrt
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
Definition: abstract_value_object.h:25
constant_abstract_valuet::to_interval
constant_interval_exprt to_interval() const override
Definition: constant_abstract_value.cpp:94
std_expr.h
API to expression classes.
constant_abstract_valuet::index_range_implementation
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
Definition: constant_abstract_value.cpp:67
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.