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 private:
28 
29 public:
30  explicit interval_abstract_valuet(const typet &t);
31  interval_abstract_valuet(const typet &t, bool tp, bool bttm);
32 
34 
36  const exprt &e,
37  const abstract_environmentt &environment,
38  const namespacet &ns);
39 
40  ~interval_abstract_valuet() override = default;
41 
42  index_range_ptrt index_range(const namespacet &ns) const override;
43 
44  exprt to_constant() const override;
45 
61  const exprt &expr,
62  const std::vector<abstract_object_pointert> &operands,
63  const abstract_environmentt &environment,
64  const namespacet &ns) const override;
65 
66  void output(
67  std::ostream &out,
68  const class ai_baset &ai,
69  const class namespacet &ns) const override;
70 
72 
73  void get_statistics(
74  abstract_object_statisticst &statistics,
75  abstract_object_visitedt &visited,
76  const abstract_environmentt &env,
77  const namespacet &ns) const override;
78 
79 protected:
80  CLONE
83  meet(const abstract_object_pointert &other) const override;
84 
85 private:
87  const exprt &expr,
88  const std::vector<interval_abstract_value_pointert> &interval_operands,
89  const abstract_environmentt &environment,
90  const namespacet &ns);
92  const exprt &expr,
93  const std::vector<interval_abstract_value_pointert> &interval_operands,
94  const abstract_environmentt &environment,
95  const namespacet &ns);
96 
101 
103 };
104 
105 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H
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:418
typet
The type of an expression, extends irept.
Definition: type.h:28
interval_abstract_valuet::evaluate_conditional
static abstract_object_pointert evaluate_conditional(const exprt &expr, const std::vector< interval_abstract_value_pointert > &interval_operands, const abstract_environmentt &environment, const namespacet &ns)
Definition: interval_abstract_value.cpp:356
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.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:252
index_range_ptrt
std::shared_ptr< index_ranget > index_range_ptrt
Definition: abstract_value_object.h:43
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
interval_abstract_valuet::expression_transform
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.
Definition: interval_abstract_value.cpp:273
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::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:526
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
abstract_value_objectt
Definition: abstract_value_object.h:50
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:568
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
interval_abstract_valuet::evaluate_unary_expr
static abstract_object_pointert evaluate_unary_expr(const exprt &expr, const std::vector< interval_abstract_value_pointert > &interval_operands, const abstract_environmentt &environment, const namespacet &ns)
Definition: interval_abstract_value.cpp:389
interval_abstract_valuet::interval_abstract_value_pointert
sharing_ptrt< interval_abstract_valuet > interval_abstract_value_pointert
Definition: interval_abstract_value.h:27
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:463
interval_abstract_valuet::get_interval
const constant_interval_exprt & get_interval() const
Definition: interval_abstract_value.cpp:563
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:221
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:506
interval_abstract_valuet::interval
constant_interval_exprt interval
Definition: interval_abstract_value.h:102
std_expr.h
API to expression classes.
interval_abstract_valuet::merge_intervals
abstract_object_pointert merge_intervals(interval_abstract_value_pointert other) const
Merge another interval abstract object with this one.
Definition: interval_abstract_value.cpp:484
abstract_objectt::t
typet t
To enforce copy-on-write these are private and have read-only accessors.
Definition: abstract_object.h:361
interval_abstract_valuet::index_range
index_range_ptrt index_range(const namespacet &ns) const override
Definition: interval_abstract_value.cpp:553
abstract_value_object.h
Common behaviour for abstract objects modelling values - constants, intervals, etc.