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 
20 {
21 public:
22  explicit constant_abstract_valuet(const typet &t);
23  explicit constant_abstract_valuet(const exprt &t);
24  constant_abstract_valuet(const typet &t, bool tp, bool bttm);
26  const exprt &e,
27  const abstract_environmentt &environment,
28  const namespacet &ns);
29 
30  ~constant_abstract_valuet() override = default;
31 
33  index_range_implementation(const namespacet &ns) const override;
34 
36 
37  exprt to_constant() const override;
38  constant_interval_exprt to_interval() const override;
39 
41  constrain(const exprt &lower, const exprt &upper) const override;
42 
43  void output(
44  std::ostream &out,
45  const class ai_baset &ai,
46  const class namespacet &ns) const override;
47 
48  void get_statistics(
49  abstract_object_statisticst &statistics,
50  abstract_object_visitedt &visited,
51  const abstract_environmentt &env,
52  const namespacet &ns) const override;
53 
54  size_t internal_hash() const override
55  {
56  return std::hash<std::string>{}(value.pretty());
57  }
58 
59  bool internal_equality(const abstract_object_pointert &other) const override
60  {
61  auto cast_other =
62  std::dynamic_pointer_cast<const constant_abstract_valuet>(other);
63  return cast_other && value == cast_other->value;
64  }
65 
66 protected:
67  CLONE
68 
78  const abstract_value_pointert &other,
79  const widen_modet &widen_mode) const override;
80 
82  meet_with_value(const abstract_value_pointert &other) const override;
83 
84  exprt to_predicate_internal(const exprt &name) const override;
85 
86 private:
88 };
89 
90 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_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.
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
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
value_range_implementation_ptrt value_range_implementation() const override
size_t internal_hash() const override
constant_interval_exprt to_interval() const override
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
~constant_abstract_valuet() override=default
abstract_value_pointert constrain(const exprt &lower, const exprt &upper) const override
exprt to_constant() const override
Converts to a constant expression if possible.
bool internal_equality(const abstract_object_pointert &other) const override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
CLONE abstract_object_pointert merge_with_value(const abstract_value_pointert &other, const widen_modet &widen_mode) const override
Merges another abstract value into this one.
abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override
Represents an interval of values.
Definition: interval.h:48
Base class for all expressions.
Definition: expr.h:54
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
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:28