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 private:
25 
26 public:
27  explicit constant_abstract_valuet(const typet &t);
28  constant_abstract_valuet(const typet &t, bool tp, bool bttm);
30  const exprt &e,
31  const abstract_environmentt &environment,
32  const namespacet &ns);
33 
34  ~constant_abstract_valuet() override = default;
35 
36  index_range_ptrt index_range(const namespacet &ns) const override;
37 
53  const exprt &expr,
54  const std::vector<abstract_object_pointert> &operands,
55  const abstract_environmentt &environment,
56  const namespacet &ns) const override;
57 
58  exprt to_constant() const override;
59 
60  void output(
61  std::ostream &out,
62  const class ai_baset &ai,
63  const class namespacet &ns) const override;
64 
65  void get_statistics(
66  abstract_object_statisticst &statistics,
67  abstract_object_visitedt &visited,
68  const abstract_environmentt &env,
69  const namespacet &ns) const override;
70 
71  size_t internal_hash() const override
72  {
73  return std::hash<std::string>{}(value.pretty());
74  }
75 
76  bool internal_equality(const abstract_object_pointert &other) const override
77  {
78  auto cast_other =
79  std::dynamic_pointer_cast<const constant_abstract_valuet>(other);
80  return cast_other && value == cast_other->value;
81  }
82 
83 protected:
84  CLONE
85 
93 
95  const exprt &expr,
96  const abstract_environmentt &environment,
97  const namespacet &ns) const;
98 
99 private:
109 
111 };
112 
113 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_ABSTRACT_VALUE_H
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
#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::shared_ptr< index_ranget > index_range_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:120
abstract_object_pointert merge_constant_constant(const constant_abstract_value_pointert &other) const
Merges another constant abstract value into this one.
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
sharing_ptrt< constant_abstract_valuet > constant_abstract_value_pointert
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
size_t internal_hash() const override
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
~constant_abstract_valuet() override=default
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...
index_range_ptrt index_range(const namespacet &ns) const override
exprt to_constant() const override
Converts to a constant expression if possible.
bool internal_equality(const abstract_object_pointert &other) const override
abstract_object_pointert try_transform_expr_with_all_rounding_modes(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) const
Base class for all expressions.
Definition: expr.h:54
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The type of an expression, extends irept.
Definition: type.h:28
API to expression classes.